diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c713a31fa..617d3d701 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3520,12 +3520,11 @@ let error_ind_scheme s = let glob c = EConstr.of_constr (Universes.constr_of_global c) -let coq_eq = lazy (glob (Coqlib.build_coq_eq ())) +let coq_eq = lazy (glob (Coqlib.build_coq_eq ())) let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ())) -let coq_heq = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")) -let coq_heq_refl = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")) - +let coq_heq = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")) +let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")) let mkEq t x y = mkApp (Lazy.force coq_eq, [| t; x; y |]) |