diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 | ||||
| -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 |
5 files changed, 6 insertions, 6 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index b9334801cd..c4d6a7a304 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -150,7 +150,7 @@ let interp_justification_items sigma env = let interp_constr check_sort sigma env c = if check_sort then - understand_type sigma env (fst c) + understand sigma env ~expected_type:IsType (fst c) else understand sigma env (fst c) @@ -175,7 +175,7 @@ let get_eq_typ info env = typ let interp_constr_in_type typ sigma env c = - understand sigma env (fst c) ~expected_type:typ + understand sigma env (fst c) ~expected_type:(OfType typ) let interp_statement interp_it sigma env st = {st_label=st.st_label; diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 5e55bcfb27..70c7f8d1fa 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1280,7 +1280,7 @@ let understand_my_constr c gls = | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand) | rc -> map_glob_constr frob rc in - Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc) let my_refine c gls = let oc = understand_my_constr c gls in 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 |