diff options
| author | Pierre-Marie Pédrot | 2018-10-19 15:27:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 15:27:55 +0200 |
| commit | 3799939088b5aa616974a0d37de7e2616024f222 (patch) | |
| tree | 808e60e5546489a694e1da784bd4895bc0195172 /plugins/firstorder/rules.ml | |
| parent | 6ab9a8088394b710ae0b9f6d5711d2fe0509419f (diff) | |
| parent | e050884da17b260934a428d5b1bb11cd788ae0e1 (diff) | |
Merge PR #8724: [universes] deprecate constr_of_global
Diffstat (limited to 'plugins/firstorder/rules.ml')
| -rw-r--r-- | plugins/firstorder/rules.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8fa676de44..b0c4785d7a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -233,12 +233,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = UnivGen.constr_of_global - @@ Coqlib.lib_ref str +let constant str = Coqlib.lib_ref str let defined_connectives = lazy - [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); - AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] + [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type")); + AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> |