gitignore and shortened cs predicate name

LPCIC · Jan 26, 2024 · 1df4d5d · 1df4d5d
1 parent f8e854f
commit 1df4d5d
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 103 deletions.
diff --git a/.gitignore b/.gitignore
@@ -48,3 +48,4 @@ META
 apps/coercion/src/coq_elpi_coercion_hook.ml
 .filestoinstall
 apps/tc/src/coq_elpi_tc_hook.ml
+apps/cs/src/coq_elpi_cs_hook.ml
diff --git a/apps/cs/src/coq_elpi_cs_hook.ml b/apps/cs/src/coq_elpi_cs_hook.ml
diff --git a/apps/cs/theories/cs.v b/apps/cs/theories/cs.v
@@ -7,7 +7,7 @@ Elpi Db cs.db lp:{{
 % - [Ctx] is the context
 % - [Lhs] and [Rhs] are the terms to unify
 :index (0 6 6)
-pred canonical-solution i:goal-ctx, o:term, o:term.
+pred cs i:goal-ctx, o:term, o:term.
 
 }}.
 
@@ -17,8 +17,8 @@ Elpi Tactic canonical_solution.
 Elpi Accumulate lp:{{
 
 solve (goal Ctx _ {{ @eq lp:T lp:Lhs lp:Rhs }} _P []) _ :-
-  canonical-solution Ctx Lhs Rhs,
-  % std.assert! (P = {{ eq_refl lp:Lhs }}) "canonical-solution wrong solution".
+  cs Ctx Lhs Rhs,
+  % std.assert! (P = {{ eq_refl lp:Lhs }}) "cs: wrong solution".
   true.
 
 }}.