diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index eabad955e..00020609e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -54,7 +54,9 @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] let coq_init_constant s = - EConstr.of_constr (Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s) + EConstr.of_constr ( + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -1223,7 +1225,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Coqlib.build_coq_and () in + let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in let conj_constr = coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in |