Remove tactic param in favor of trocq

coq-community · Jan 2, 2024 · aafb249 · aafb249
1 parent 38792d2
commit aafb249
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git 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
@@ -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.
-Original file line number
+Diff line change
@@ Expand Up / @@ -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.