diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
4 files changed, 5 insertions, 0 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index cc29d68f59..c98cdc4678 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -985,6 +985,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in + let t = EConstr.Unsafe.to_constr t in decompose_prod_n_assum (nb_params + nb_args) t,evd in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 38cd21684a..0725bb11c1 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1273,6 +1273,7 @@ let do_build_inductive Array.fold_right2 (fun id c (evd,env) -> let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in + let t = EConstr.Unsafe.to_constr t in evd, Environ.push_named (LocalAssum (id,t)) (* try *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 37a76bec1c..1b899c152f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -373,6 +373,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in + let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd interactive_proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ca066c4cca..27528c2dcc 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 |