diff options
| author | Pierre-Marie Pédrot | 2018-05-17 17:43:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-17 17:43:37 +0200 |
| commit | b0cf6c4042ed8e91c6f7081a6f0c4b83ec9407c2 (patch) | |
| tree | 7f0cd1ed2217f826c0d64f6a0fa700f506dd8e86 /plugins/funind/invfun.ml | |
| parent | 78c8d75e38844cb88c551881112e10728962dc2d (diff) | |
| parent | 9f175bbeb19175a1e422225986f139e8f1a1b56c (diff) | |
Merge PR #7359: Reduce usage of evar_map references
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 |