diff options
Diffstat (limited to 'tactics/eqschemes.ml')
| -rw-r--r-- | tactics/eqschemes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index ea5ff4a6cb..16b94cd154 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -99,7 +99,7 @@ let my_it_mkLambda_or_LetIn_name s c = let get_coq_eq ctx = try - let eq = Globnames.destIndRef Coqlib.glob_eq in + let eq = Globnames.destIndRef (Coqlib.lib_ref "core.eq.type") in (* Do not force the lazy if they are not defined *) let eq, ctx = with_context_set ctx (UnivGen.fresh_inductive_instance (Global.env ()) eq) in |