From e13be8b419fb0847cfe224c920ca34d2501b4401 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 1 Dec 2024 21:38:20 +0100
Subject: [PATCH 1/3] typcheck type

---
 examples/example_open_terms.v | 4 +++-
 tests/test_open_terms.v       | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/examples/example_open_terms.v b/examples/example_open_terms.v
index 673c8b088..094d5b3be 100644
--- 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 }}}} :- !,
diff --git a/tests/test_open_terms.v b/tests/test_open_terms.v
index 5de1b5bfb..5e23b9b87 100644
--- 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,!,

From 8a540c36f4c2c0e7e2d9ca18526983f24d914aad Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 1 Dec 2024 21:42:38 +0100
Subject: [PATCH 2/3] re-enable tests

---
 examples/example_open_terms.v | 4 ++--
 tests/test_open_terms.v       | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/examples/example_open_terms.v b/examples/example_open_terms.v
index 094d5b3be..5bdb6b65c 100644
--- a/examples/example_open_terms.v
+++ b/examples/example_open_terms.v
@@ -221,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.
@@ -235,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
index 5e23b9b87..a15cfc780 100644
--- a/tests/test_open_terms.v
+++ b/tests/test_open_terms.v
@@ -296,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.
@@ -413,4 +412,4 @@ now apply map_ext_in; intros a _; ring.
 Qed.
 
 End sandbox.
-  *)
+

From 4adba1abe75fd1de8c56cb77efb49599dbe0149e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 1 Dec 2024 22:39:25 +0100
Subject: [PATCH 3/3] ci

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 609b027bf..f8147c217 100644
--- 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