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/funind/invfun.ml | |
| parent | 6ab9a8088394b710ae0b9f6d5711d2fe0509419f (diff) | |
| parent | e050884da17b260934a428d5b1bb11cd788ae0e1 (diff) | |
Merge PR #8724: [universes] deprecate constr_of_global
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b8973a18dc..b0842c3721 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ |