From aafb2499b65f7884489c0d528dd65c339f643a96 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 2 Jan 2024 09:47:26 +0100 Subject: [PATCH] Remove tactic param in favor of trocq --- examples/Example.v | 2 +- theories/Param.v | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/examples/Example.v b/examples/Example.v index 28fc1e8..0744d48 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -51,5 +51,5 @@ Goal (* forall (X : forall (A : Type@{i}), A -> Type@{i}) (A : Type@{i}) (a : A), A -> X A a -> A. *) (* forall (T : (Type@{i} -> Type@{j})) (F : ((Type@{i} -> Type@{j}) -> Type@{k})), F T. *) Proof. - param. + trocq. Abort. diff --git a/theories/Param.v b/theories/Param.v index 42117b8..30a3049 100644 --- a/theories/Param.v +++ b/theories/Param.v @@ -140,7 +140,7 @@ Elpi Query lp:{{ ). }}. -Elpi Tactic param. +Elpi Tactic trocq. Elpi Accumulate Db trocq.db. Elpi Accumulate File annot. Elpi Accumulate File util. @@ -201,5 +201,4 @@ Elpi Accumulate lp:{{ }}. Elpi Typecheck. -Tactic Notation "param" := elpi param. -Tactic Notation "trocq" := elpi param. +Tactic Notation "trocq" := elpi trocq.