diff options
| author | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
| commit | 15998894ff76b1fa9354085ea0bddae4f8f23ddf (patch) | |
| tree | 254cc3a53b6aa344f49a10cba32e14acf97d2905 /plugins/funind/recdef.ml | |
| parent | 063cf49f40511730c8c60c45332e92823ce4c78f (diff) | |
| parent | 6aa0aa37e19457a8c0c3ad36f7bbead058442344 (diff) | |
Merge PR #8694: Various cleanups of universe apis
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 9fa333c629..ca3160f4c4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -24,6 +24,7 @@ open Globnames open Nameops open CErrors open Util +open UnivGen open Tacticals open Tacmach open Tactics @@ -50,7 +51,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) [@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ constr_of_global @@ Coqlib.find_reference "RecursiveDefinition" m s let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] @@ -62,7 +63,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - UnivGen.constr_of_global @@ + constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) [@@@ocaml.warning "+3"] @@ -96,9 +97,6 @@ let type_of_const sigma t = Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false -let constr_of_global x = - fst (Global.constr_of_global_in_context (Global.env ()) x) - let constant sl s = constr_of_global (find_reference sl s) let const_of_ref = function |