4 files changed, 8 insertions, 6 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index e0aee15e6..541b59920 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -316,7 +316,7 @@ let rec match_aliases names constr = function
       let args,bnames,body = match_aliases qnames body q in
 	st::args,bnames,body
 
-let detype_ground c = Detyping.detype false [] [] c
+let detype_ground c = Detyping.detype false [] [] Evd.empty c
 
 let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index b5566127f..c5a474d39 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
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a930245b6..9d909fda3 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -26,8 +26,8 @@ let pr_goal gs =
   let preamb,thesis,penv,pc =
     (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
     (str "thesis := "  ++ fnl ()),
-    Printer.pr_context_of env,
-    Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g)
+    Printer.pr_context_of env sigma,
+    Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 7f63c4200..be2e44cff 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -20,6 +20,8 @@ let pr_label = function
     Anonymous -> mt ()
   | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
 
+let pr_constr env c = pr_constr env Evd.empty c
+
 let pr_justification_items env = function
     Some [] -> mt ()
   | Some (_::_ as l) ->