diff options
| author | Pierre-Marie Pédrot | 2018-05-22 17:22:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-22 17:22:52 +0200 |
| commit | c792c9fc500cbc1cab14271ebc6a98cd516451b3 (patch) | |
| tree | a3ef08574a31fe1eec2ac6a5194d667789c33625 /plugins/funind/recdef.ml | |
| parent | c3838b204d3db7a58246d960a3da7efb7d1cc2f2 (diff) | |
| parent | 748a33cee41900d285897b24b4d8e29dd9eb2a3d (diff) | |
Merge PR #7384: Split 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 2a3a85fcc0..2464c595f5 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 |