Skip to content

Commit

Permalink
Adapt to coq/coq#19310
Browse files Browse the repository at this point in the history
  • Loading branch information
proux01 committed Jul 14, 2024
1 parent 56b874c commit 34b3bad
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 3 deletions.
1 change: 1 addition & 0 deletions apps/coercion/tests/coercion.t/test.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
From elpi.apps Require Import coercion.
#[warning="-deprecated-from-Coq"]
From Coq Require Import Bool.

Elpi Accumulate coercion.db lp:{{
Expand Down
1 change: 1 addition & 0 deletions apps/coercion/tests/coercion_open.t/test.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
From elpi.apps Require Import coercion.
#[warning="-deprecated-from-Coq"]
From Coq Require Import Arith ssreflect.

Ltac my_solver := trivial with arith.
Expand Down
15 changes: 12 additions & 3 deletions apps/tc/tests/bigTest.v
Original file line number Diff line number Diff line change
Expand Up @@ -882,14 +882,23 @@ instances *)
Section prod_setoid.
Context `{Equiv A, Equiv B}.
Elpi Accumulate TC.Solver lp:{{
shorten tc-Coq.Classes.RelationClasses.{tc-Equivalence}.
/* uncomment when requiring Coq >= 8.21
shorten tc-Stdlib.Classes.RelationClasses.{tc-Equivalence}. */
/* remove below definition when requiring Coq >= 8.21 */
:after "lastHook"
tc-Equivalence A RA R :-
tc-Coq.Classes.RelationClasses.tc-Equivalence A RA R :-
RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
RA' = {{@prod_relation _ _ _ _}},
coq.unify-eq RA RA' ok,
% coq.say A RA,
tc-Equivalence A RA' R.
tc-Coq.Classes.RelationClasses.tc-Equivalence A RA' R.
:after "lastHook"
tc-Stdlib.Classes.RelationClasses.tc-Equivalence A RA R :-
RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
RA' = {{@prod_relation _ _ _ _}},
coq.unify-eq RA RA' ok,
% coq.say A RA,
tc-Stdlib.Classes.RelationClasses.tc-Equivalence A RA' R.
}}.
(* Elpi Typecheck TC.Solver. *)

Expand Down

0 comments on commit 34b3bad

Please sign in to comment.