3 files changed, 9 insertions, 7 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 34fea6175b..8b9eb39837 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -471,7 +471,7 @@ END
 
 VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
 | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
-  [ VtUnknown, VtNow ] ->
+  [ VtSideff [], VtNow ] ->
   [ fun ~atts ~st -> let open Vernacinterp in
       let n = Option.default 0 n in
       Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index ee34161dd7..2e14243d8a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2021,14 +2021,16 @@ let add_morphism glob binders m s n =
 (** Taken from original setoid_replace, to emulate the old rewrite semantics where
     lemmas are first instantiated and then rewrite proceeds. *)
 
-let check_evar_map_of_evars_defs evd =
+let check_evar_map_of_evars_defs env evd =
  let metas = Evd.meta_list evd in
  let check_freemetas_is_empty rebus =
   Evd.Metaset.iter
    (fun m ->
-     if Evd.meta_defined evd m then () else
-      raise
-	(Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
+     if Evd.meta_defined evd m then ()
+     else begin
+       raise
+         (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m]))
+     end)
  in
   List.iter
    (fun (_,binding) ->
@@ -2063,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
   let c1 = if l2r then nf c' else nf c1
   and c2 = if l2r then nf c2 else nf c'
   and car = nf car and rel = nf rel in
-  check_evar_map_of_evars_defs sigma;
+  check_evar_map_of_evars_defs env sigma;
   let prf = nf prf in
   let prfty = nf (Retyping.get_type_of env sigma prf) in
   let sort = sort_of_rel env sigma but in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e0d7eca5f8..9e47db1c34 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id))
+  else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id))
 
 let interp_hyp_list_as_list ist env sigma (loc,id as x) =
   try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)