diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 17:15:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | 531590c223af42c07a93142ab0cea470a98964e6 (patch) | |
| tree | bfe531d8d32e491a66eceba60995702e20e73757 /plugins/funind/invfun.ml | |
| parent | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (diff) | |
Removing compatibility layers in Retyping
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ca066c4cc..27528c2dc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -135,6 +135,7 @@ let generate_type evd g_to_f f graph i = in evd:=evd'; let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in + let graph_arity = EConstr.Unsafe.to_constr graph_arity in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -203,6 +204,7 @@ let find_induction_principle evd f = | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in + let typ = EConstr.Unsafe.to_constr typ in evd:=evd'; rect_lemma,typ |