diff options
author | 2017-05-28 21:54:11 +0200 | |
---|---|---|
committer | 2017-05-28 21:54:11 +0200 | |
commit | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (patch) | |
tree | aea1f671a7486d7449ad6883f08e6e9a2ce4f744 /plugins/funind/recdef.ml | |
parent | fe62902764cc52daa985ad03e6f7ac0f8f1c2c4c (diff) | |
parent | 5cc13770ac2358d583b21f217b8c65d2d5abd850 (diff) |
Merge PR#678: [coqlib] Move `Coqlib` to `library/`.
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 |