diff options
| author | Gaëtan Gilbert | 2018-04-26 15:03:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-14 13:25:56 +0200 |
| commit | c22ac10752c12bcb23402ad29a73f2d9699248a6 (patch) | |
| tree | 9a77251356af06e08c70f46235815f6a6d4c2bfb /plugins/funind/invfun.ml | |
| parent | e68f8c904b7ee8fee9f98f75e37ab6d01b54731f (diff) | |
Deprecate Typing.e_* functions
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 28e85268a3..094f54156b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -103,7 +103,8 @@ let generate_type evd g_to_f f graph i = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) in evd:=evd'; - let graph_arity = Typing.e_type_of (Global.env ()) evd graph in + let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in + evd := sigma; let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with @@ -769,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in + let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in + evd := sigma; let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info |