diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index cc29d68f5..c98cdc467 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 |