diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 15:50:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (patch) | |
| tree | 4ab6481d8d182f6bb3dd241b7112a3027aa26b2a /plugins/funind/invfun.ml | |
| parent | ffb59901f568351401f2f3d1f3334031658b8880 (diff) | |
Removing some return type compatibility layers in Termops.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c02b64c1f..ca066c4cc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -399,8 +399,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes match ctxt with | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") | hres::res::decl::ctxt -> - let res = Termops.it_mkLambda_or_LetIn - (Termops.it_mkProd_or_LetIn concl [hres;res]) + let res = Term.it_mkLambda_or_LetIn + (Term.it_mkProd_or_LetIn concl [hres;res]) (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) in res @@ -793,7 +793,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( in let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; - let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in + let type_of_lemma = Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in @@ -861,7 +861,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = - Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt + Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in |