diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 |
2 files changed, 3 insertions, 3 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 |