Merge pull request #724 from LPCIC/fix-open-term

typcheck type
LPCIC · Dec 1, 2024 · 9f73e90 · 9f73e90
2 parents 6565e29 + 4adba1a
commit 9f73e90
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -49,7 +49,7 @@ jobs:
         opam pin add coq-core ${{ matrix.coq_version }}
         opam pin add coq-stdlib ${{ matrix.coq_version }}
       if: ${{ matrix.coq_version != 'dev' }}
-    - run: opam install ./coq-elpi.opam --deps-only --with-test -y
+    - run: opam install ./coq-elpi.opam --deps-only --with-test -y --ignore-constraints-on coq 
     - run: opam exec make build
     - run: opam exec make test
 

diff --git a/examples/example_open_terms.v b/examples/example_open_terms.v
@@ -181,7 +181,9 @@ pred replace i:argument, i:argument, i:term, o:term, o:term.
 % all binders are crossed and we find a term identical to L.
 % the proof is a hole of type L = R.
 replace (open-trm 0 L) (open-trm 0 R) L R P :- !,
-  coq.typecheck P {{ lp:L = lp:R }} ok.
+  TY = {{ lp:L = lp:R }},
+  coq.typecheck-ty TY _ ok,
+  coq.typecheck P TY ok.
 
 % we cross the binder by functional extensionality
 replace L R (fun N T F) (fun N T F1) {{ functional_extensionality lp:{{ fun N T F }} lp:{{ fun N T F1 }} lp:{{ fun N T Prf }}}} :- !,
@@ -219,7 +221,7 @@ Tactic Notation (at level 0) "repl" uconstr(x) "with" uconstr(y) :=
 
 Tactic Notation (at level 0) "repl" uconstr(x) "with" uconstr(y) "by" tactic(t) :=
   elpi replace ltac_open_term:(x) ltac_open_term:(y); try (simpl; t).
-   (*
+
 Lemma hard_example : forall l, map (fun x => x + 1) l = map (fun x => 1 + x) l.
 Proof.
   intros l.
@@ -233,6 +235,6 @@ Proof.
   repl (x + 0 + y) with (y + x) by ring.
   reflexivity.
 Qed.
-      *)
+
 (* An extended version of this tactic by Y. Bertot can be found in the tests/
    directory under the name test_open_terms.v *)
diff --git a/tests/test_open_terms.v b/tests/test_open_terms.v
@@ -150,7 +150,9 @@ instantiate_pair N T C (pr A1 A2) (pr B1 B2) :-
 pred mk-equality i:(pair argument argument), i:term i:A, o:term, o:term, o:A.
 
 mk-equality (pr (open-trm 0 S) (open-trm 0 T)) S A T P A :- !,
-  coq.typecheck P {{lp:S = lp:T}} ok.
+  TY = {{lp:S = lp:T}},
+  coq.typecheck-ty TY _ ok,
+  coq.typecheck P TY ok.
 
 :name "mk-equality:start"
 mk-equality _RW X A Z Y A :- name X,!,
@@ -294,7 +296,6 @@ Open Scope Z_scope. (* Otherwise ring fails. *)
   but they all have to be fillable with bound variables where the binding
   happens in the goal, in a nested fashion. *)
 
-    (*
 (* This test illustrates the case where there is no unknown. *)
 Goal forall x, x = 1 -> 2 = x + 1.
 intros x x1.
@@ -411,4 +412,4 @@ now apply map_ext_in; intros a _; ring.
 Qed.
 
 End sandbox.
-  *)
+