fix tests

Author: gares

apps/coercion/README.md

@@ -36,7 +36,6 @@ coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
 coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
 
 }}.
-Elpi Typecheck coercion. (* checks the elpi program is OK *)
 
 Check True && False.
 ```

apps/coercion/tests/coercion.t/test.v

@@ -8,7 +8,6 @@ coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
 coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
 
 }}.
-Elpi Typecheck coercion.
 
 Check True && False.
 
@@ -22,7 +21,6 @@ coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :-
   coq.typecheck R {{ ringType }} ok.
 
 }}.
-Elpi Typecheck coercion.
 
 Section TestNatMul.
 

apps/coercion/tests/coercion_open.t/test.v

@@ -4,7 +4,7 @@ From Coq Require Import Arith ssreflect.
 
 Ltac my_solver := trivial with arith.
 
-Elpi Accumulate coercion.db lp:{{
+Elpi Accumulate coercion lp:{{
 
 coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   % we unfold letins since the solve is dumb
@@ -17,7 +17,6 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
 ].
 
 }}.
-Elpi Typecheck coercion.
 
 Goal {x : nat | x > 0}.
 apply: 3.

apps/cs/README.md

@@ -38,7 +38,6 @@ cs _ {{ sort lp:Sol }} {{ nat }} :-
   Sol = {{ Build_S nat }}.
 
 }}.
-Elpi Typecheck canonical_solution.
 
 Check eq_refl _ : (sort _) = nat.
 ```

apps/cs/tests/cs.t.disabled_broken_8.19/test.v

@@ -9,7 +9,6 @@ Elpi Accumulate canonical_solution lp:{{
 cs _ {{ sort lp:T }} {{ @id lp:T }} {{ Build_S lp:T (@id lp:T) }}.
 
 }}.
-Elpi Typecheck canonical_solution.
 
 Check 1.
 Check eq_refl _ : (sort nat _) = @id nat.

apps/derive/README.md

@@ -575,7 +575,6 @@ From elpi.apps Require Export
   ...
   myder (* new derivation *)
 . 
-Elpi Typecheck derive.
 ```
 
 So when the user `Import`s `better_std` he gets a fully loaded `derive`.

examples/tutorial_coq_elpi_tactic.v

@@ -92,11 +92,12 @@ is stored in the .vo file (the external file does not need to be installed).
 We invite the reader to look up the description of data bases in the tutorial
 about commands.
   
-Once all the code is accumulated `Elpi Typecheck` verifies that the
-code does not contain the most frequent kind of mistakes. This command
-considers some mistakes minor and only warns about them. You can
-pass `-w +elpi.typecheck` to `coqc` to turn these warnings into errors.
-  
+When some code is accumulated Elpi verifies that the
+code does not contain the most frequent kind of mistakes, via some
+type checking and linting. Some mistakes are minor and Elpi only warns about
+them. You can pass `-w +elpi.typecheck` to `coqc` to turn these warnings into
+errors.
+
 The entry point for tactics is called :builtin:`solve` which maps a :type:`goal`
 into a list of :type:`sealed-goal` (representing subgoals).