diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 19:26:21 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
commit | a51dda2344679dc6d9145f3f34acad29721f6c75 (patch) | |
tree | c9ed50095ae459dabd97d9571566647439cf5269 /plugins/funind/recdef.ml | |
parent | b0ef649660542ae840ea945d7ab4f1f3ae7b85cd (diff) |
Split off Universes functions dealing with generating new universes.
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r-- | plugins/funind/recdef.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2a3a85fcc..2464c595f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -49,7 +49,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ Coqlib.coq_reference "RecursiveDefinition" m s let arith_Nat = ["Arith";"PeanoNat";"Nat"] @@ -61,7 +61,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = @@ -1241,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in + let and_constr = UnivGen.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 |