diff options
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.ml')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b5566127f1..c5a474d39f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1034,12 +1034,12 @@ let thesis_for obj typ per_info env= let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in compose_prod rc (Reductionops.whd_beta Evd.empty hd2) @@ -1273,7 +1273,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let understand_my_constr c gls = let env = pf_env gls in let nc = names_of_rel_context env in - let rawc = Detyping.detype false [] nc c in + let rawc = Detyping.detype false [] nc Evd.empty c in let rec frob = function | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None) | rc -> map_glob_constr frob rc |