diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e98a0952b9..e1de8be82a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -334,7 +334,7 @@ let raw_push_named (na,raw_value,raw_typ) env = | Anonymous -> env | Name id -> let value = Option.map (Pretyping.understand Evd.empty env) raw_value in - let typ = Pretyping.understand_type Evd.empty env raw_typ in + let typ = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in Environ.push_named (id,value,typ) env diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index fcd1c5360e..2a0bbd7b78 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -131,7 +131,7 @@ let rec abstract_glob_constr c = function (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = - Constrintern.intern_gen (Pretyping.OfType None) sigma env ~impls + Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls ~allow_patvar:false ~ltacvars:([],[]) c (* diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 34085dca2f..4b9704c2c9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1449,7 +1449,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let equation_lemma_type = nf_betaiotazeta - (interp_gen (OfType None) Evd.empty env ~impls:rec_impls eq) + (interp_constr Evd.empty env ~impls:rec_impls eq) in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in |