Merge branch 'v8.5'

18 files changed, 154 insertions, 132 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 46274f8329..7da8415714 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -131,7 +131,7 @@ let conclPattern concl pat tac =
 	try
 	  Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
 	with Constr_matching.PatternMatchingFailure ->
-          Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
+          Tacticals.New.tclZEROMSG (str "conclPattern")
   in
    Proofview.Goal.enter (fun gl ->
      let env = Proofview.Goal.env gl in
@@ -458,7 +458,7 @@ let search d n mod_delta db_list local_db =
     (* spiwack: the test of [n] to 0 must be done independently in
        each goal. Hence the [tclEXTEND] *)
     Proofview.tclEXTEND [] begin
-      if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
+      if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
         Tacticals.New.tclORELSE0 (dbg_assumption d)
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4eb8a79256..ad8164fa64 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -66,7 +66,7 @@ let find_base bas =
   try raw_find_base bas
   with Not_found ->
     errorlabstrm "AutoRewrite"
-      (str ("Rewriting base "^(bas)^" does not exist."))
+      (str "Rewriting base " ++ str bas ++ str " does not exist.")
 
 let find_rewrites bas =
   List.rev_map snd (HintDN.find_all (find_base bas))
@@ -174,7 +174,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
   if cl.concl_occs != AllOccurrences &&
      cl.concl_occs != NoOccurrences
   then
-    Proofview.tclZERO (UserError("" , str"The \"at\" syntax isn't available yet for the autorewrite tactic."))
+    Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
   else
     let compose_tac t1 t2 =
       match cl.onhyps with
@@ -204,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
 	*)
 	gen_auto_multi_rewrite conds tac_main lbas cl
     | _ ->
-        Proofview.tclZERO (UserError ("autorewrite",strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion."))
+        Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 1f5177c3d5..b87d657539 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -144,7 +144,7 @@ struct
 
  type t = Dn.t
 
-  let create = Dn.create
+  let empty = Dn.empty
 
   let add = function
     | None ->
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 6c396b4c8b..f29d186153 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -28,7 +28,7 @@ module Make :
 sig
   type t
 
-  val create : unit ->  t
+  val empty : t
 
   val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t
   val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9b69481da9..c03710e911 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -55,7 +55,7 @@ let contradiction_context =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
-      | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
+      | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
       | (id,_,typ)::rest ->
           let typ = nf_evar sigma typ in
 	  let typ = whd_betadeltaiota env sigma typ in
@@ -107,7 +107,7 @@ let contradiction_term (c,lbind as cl) =
             Proofview.tclZERO Not_found
         end
         begin function (e, info) -> match e with
-          | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+          | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
           | e -> Proofview.tclZERO ~info e
         end
   end
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 3b1614d6ce..aed2c28323 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -38,7 +38,7 @@ struct
 
   type  t = Trie.t
 
-  let create () = Trie.empty
+  let empty = Trie.empty
 
 (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in
 prefix ordering, [dna] is the function returning the main node of a pattern *)
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 20407e9d97..2a60c3eb82 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -10,7 +10,7 @@ sig
 
   type t
 
-  val create : unit -> t
+  val empty : t
 
   (** [add t f (tree,inf)] adds a structured object [tree] together with
      the associated information [inf] to the table [t]; the function
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 607664486b..bd55e6fb1e 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -619,7 +619,7 @@ TACTIC EXTEND unify
     match table with
     | None ->
       let msg = str "Hint table " ++ str base ++ str " not found" in
-      Proofview.tclZERO (UserError ("", msg))
+      Tacticals.New.tclZEROMSG msg
     | Some t ->
       let state = Hint_db.transparent_state t in
       unify ~state x y
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index c2cd9e47f1..2ee4bf8e12 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -158,7 +158,7 @@ let solveEqBranch rectype =
       end
     end
     begin function (e, info) -> match e with
-      | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
+      | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -186,7 +186,7 @@ let decideGralEquality =
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure ->
-          Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."))
+          Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")
       | e -> Proofview.tclZERO ~info e
     end
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ab8d0c3ba..f2860a2300 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -306,8 +306,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
-	      let rwr_thm = Label.to_string l' in 
-	      error ("Cannot find rewrite principle "^rwr_thm^".")
+	      errorlabstrm "Equality.find_elim"
+                (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
         end
@@ -454,7 +454,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	(* Otherwise, if we are told to rewrite in all hypothesis via the
            syntax "* |-", we fail iff all the different rewrites fail *)
 	let rec do_hyps_atleastonce = function
-	  | [] -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Nothing to rewrite."))
+	  | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.")
 	  | id :: l ->
 	    tclIFTHENTRYELSEMUST
 	     (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
@@ -874,7 +874,7 @@ let gen_absurdity id =
   then
     simplest_elim (mkVar id)
   else
-    Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality."))
+    tclZEROMSG (str "Not the negation of an equality.")
   end
 
 (* Precondition: eq is leibniz equality
@@ -936,7 +936,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
     let concl = Proofview.Goal.concl gl in
     match find_positions env sigma t1 t2 with
     | Inr _ ->
-	Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
+	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
 	let sort = pf_apply get_type_of gl concl in
 	discr_positions env sigma u eq_clause cpath dirn sort
@@ -968,7 +968,7 @@ let onNegatedEquality with_evars tac =
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
-        Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+        tclZEROMSG (str "Not a negated primitive equality.")
   end
 
 let discrSimpleClause with_evars = function
@@ -1303,7 +1303,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   in
   let injectors = List.map_filter filter posns in
   if List.is_empty injectors then
-    Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
+    tclZEROMSG (str "Failed to decompose the equality.")
   else
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
     (Proofview.tclBIND
@@ -1319,12 +1319,12 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
   | Inl _ ->
-     Proofview.tclZERO (Errors.UserError ("Inj",strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal."))
+     tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
   | Inr [] ->
      let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in
-     Proofview.tclZERO (Errors.UserError ("Equality.inj",strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)))
+     tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
   | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
-     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
+     tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
 	(tac (clenv_value eq_clause))
@@ -1589,10 +1589,10 @@ let is_eq_x gl x (id,_,c) =
    erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let hyps = Proofview.Goal.hyps gl in
-  let concl = Proofview.Goal.concl gl in
+  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
   let dephyps =
     List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) ->
@@ -1663,24 +1663,45 @@ let default_subst_tactic_flags () =
     { only_leibniz = true; rewrite_dependent_proof = false }
 
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
-  Proofview.Goal.nf_enter begin fun gl ->
-  let find_eq_data_decompose = find_eq_data_decompose gl in
-  let test (_,c) =
-    try
-      let lbeq,u,(_,x,y) = find_eq_data_decompose c in
-      let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
-      if flags.only_leibniz then restrict_to_eq_and_identity eq;
-      (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-      if Term.eq_constr x y then failwith "caught";
-      match kind_of_term x with Var x -> x | _ ->
-      match kind_of_term y with Var y -> y | _ -> failwith "caught"
-    with Constr_matching.PatternMatchingFailure -> failwith "caught"
+
+  (* First step: find hypotheses to treat in linear time *)
+  let find_equations gl =
+    let gl = Proofview.Goal.assume gl in
+    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let test (hyp,_,c) =
+      try
+        let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+        let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+        if flags.only_leibniz then restrict_to_eq_and_identity eq;
+        (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+        if Term.eq_constr x y then None else
+        match kind_of_term x, kind_of_term y with
+        | Var _, _ | _, Var _ -> Some hyp
+        | _ -> None
+      with Constr_matching.PatternMatchingFailure -> None
+    in
+    let hyps = Proofview.Goal.hyps gl in
+    List.map_filter test hyps
+  in
+
+  (* Second step: treat equations *)
+  let process hyp =
+    Proofview.Goal.enter begin fun gl ->
+    let gl = Proofview.Goal.assume gl in
+    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let (_,_,c) = pf_get_hyp hyp gl in
+    let _,_,(_,x,y) = find_eq_data_decompose c in
+    (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+    if Term.eq_constr x y then Proofview.tclUNIT () else
+      match kind_of_term x, kind_of_term y with
+      | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true)
+      | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false)
+      | _ -> Proofview.tclUNIT ()
+    end
   in
-  let test p = try Some (test p) with Failure _ -> None in
-  let hyps = pf_hyps_types gl in
-  let ids = List.map_filter test hyps in
-  let ids = List.uniquize ids in
-  subst_gen flags.rewrite_dependent_proof ids
+  Proofview.Goal.nf_enter begin fun gl ->
+    let ids = find_equations gl in
+    tclMAP process ids
   end
 
 (* Rewrite the first assumption for which a condition holds
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 891e2dba51..f217cda894 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -750,7 +750,7 @@ let rec find_a_destructable_match t =
 
 let destauto t =
   try find_a_destructable_match t;
-    Proofview.tclZERO (UserError ("",  str"No destructable match found"))
+    Tacticals.New.tclZEROMSG (str "No destructable match found")
   with Found tac -> tac
 
 let destauto_in id = 
@@ -772,7 +772,7 @@ END
 let eq_constr x y = 
   Proofview.Goal.enter (fun gl ->
     let evd = Proofview.Goal.sigma gl in
-      if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () 
+      if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () 
       else Tacticals.New.tclFAIL 0 (str "Not equal"))
 
 TACTIC EXTEND constr_eq
@@ -966,7 +966,7 @@ let guard tst =
     Proofview.tclUNIT ()
   else
     let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in
-    Proofview.tclZERO (Errors.UserError("guard",msg))
+    Tacticals.New.tclZEROMSG msg
 
 
 TACTIC EXTEND guard
diff --git a/tactics/hints.ml b/tactics/hints.ml
index dea47794ec..f83aa56017 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -171,7 +171,7 @@ type search_entry = {
 let empty_se = {
   sentry_nopat = [];
   sentry_pat = [];
-  sentry_bnet = Bounded_net.create ();
+  sentry_bnet = Bounded_net.empty;
   sentry_mode = [];
 }
 
@@ -206,7 +206,7 @@ let rebuild_dn st se =
   let dn' = 
     List.fold_left 
       (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
-      (Bounded_net.create ()) se.sentry_pat
+      Bounded_net.empty se.sentry_pat
   in
   { se with sentry_bnet = dn' }
 
@@ -394,7 +394,7 @@ module Hint_db = struct
     hintdb_state : Names.transparent_state;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
-    mutable hintdb_max_id : int;
+    hintdb_max_id : int;
     use_dn : bool;
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
@@ -402,8 +402,9 @@ module Hint_db = struct
     hintdb_nopat : (global_reference option * stored_data) list
   }
 
-  let next_hint_id t = 
-    let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h
+  let next_hint_id db =
+    let h = db.hintdb_max_id in
+    { db with hintdb_max_id = succ db.hintdb_max_id }, h
 
   let empty st use_dn = { hintdb_state = st;
 			  hintdb_cut = PathEmpty;
@@ -510,8 +511,9 @@ module Hint_db = struct
 	    state, { db with hintdb_unfolds = unfs }, true
       | _ -> db.hintdb_state, db, false
     in
-    let db = if db.use_dn && rebuild then rebuild_db st' db else db
-    in addkv k (next_hint_id db) v db
+    let db = if db.use_dn && rebuild then rebuild_db st' db else db in
+    let db, id = next_hint_id db in
+    addkv k id v db
 
   let add_list l db = List.fold_left (fun db k -> add_one k db) db l
 
@@ -596,7 +598,7 @@ let current_pure_db () =
   List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
 
 let error_no_such_hint_database x =
-  error ("No such Hint database: "^x^".")
+  errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ac8b4923e5..60ce0e0dc3 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -52,7 +52,7 @@ let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
     try Nametab.global_of_path sp
     with Not_found -> 
-      anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting"))
+      anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
 
 let find_reference dir s =
   let gr = lazy (try_find_global_reference dir s) in
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 53f3f5652c..e8cb8c63bc 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -43,7 +43,7 @@ end
 module MLTacMap = Map.Make(MLName)
 
 let pr_tacname t =
-  t.mltac_plugin ^ "::" ^ t.mltac_tactic
+  str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic
 
 let tac_tab = ref MLTacMap.empty
 
@@ -52,9 +52,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
     if MLTacMap.mem s !tac_tab then
       if overwrite then
         let () = tac_tab := MLTacMap.remove s !tac_tab in
-        msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
+        msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s)
       else
-        Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
+        Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
@@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
     tacs.(i)
   with Not_found ->
     Errors.errorlabstrm ""
-      (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
+      (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
 (* Tactic registration *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f29680e185..7ce158fd1a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1040,8 +1040,8 @@ let read_pattern lfun ist env sigma = function
 let cons_and_check_name id l =
   if Id.List.mem id l then
     user_err_loc (dloc,"read_match_goal_hyps",
-      strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^
-      " used twice in the same pattern."))
+      str "Hypothesis pattern-matching variable " ++ pr_id id ++
+      str " used twice in the same pattern.")
   else id::l
 
 let rec read_match_goal_hyps lfun ist env sigma lidh = function
@@ -1492,11 +1492,11 @@ and tactic_of_value ist vle =
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       catch_error_tac trace tac
-  | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected."))
+  | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
     eval_tactic ist tac
-  else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
+  else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist llc u =
@@ -1752,10 +1752,8 @@ and interp_ltac_constr ist e : constr Ftactic.t =
     Ftactic.return cresult
   with CannotCoerceTo _ ->
     let env = Proofview.Goal.env gl in
-    Proofview.tclZERO (UserError ( "",
-      errorlabstrm ""
-      (str "Must evaluate to a closed term" ++ fnl() ++
-      str "offending expression: " ++ fnl() ++ pr_inspect env e result)))
+    Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
+      str "offending expression: " ++ fnl() ++ pr_inspect env e result)
   end
 
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9b16fe3f7b..5ba53a7641 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -420,7 +420,7 @@ module New = struct
 
   (* Try the first tactic that does not fail in a list of tactics *)
   let rec tclFIRST = function
-    | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic."))
+    | [] -> tclZEROMSG (str"No applicable tactic.")
     |  t::rest -> tclORELSE0 t (tclFIRST rest)
 
   let rec tclFIRST_PROGRESS_ON tac = function
@@ -430,10 +430,7 @@ module New = struct
 
   let rec tclDO n t =
     if n < 0 then
-      tclZERO (Errors.UserError (
-        "Refiner.tclDO",
-        str"Wrong argument : Do needs a positive integer.")
-      )
+      tclZEROMSG (str"Wrong argument : Do needs a positive integer.")
     else if n = 0 then tclUNIT ()
     else if n = 1 then t
     else tclTHEN t (tclDO (n-1) t)
@@ -456,7 +453,7 @@ module New = struct
   let tclCOMPLETE t =
     t >>= fun res ->
       (tclINDEPENDENT
-         (tclZERO (Errors.UserError ("",str"Proof is not complete.")))
+         (tclZEROMSG (str"Proof is not complete."))
       ) <*>
         tclUNIT res
 
@@ -618,7 +615,8 @@ module New = struct
 	    | Var id -> string_of_id id
 	    | _ -> "\b"
 	  in
-	  error ("The elimination combinator " ^ name_elim ^ " is unknown.")
+	  errorlabstrm "Tacticals.general_elim_then_using"
+            (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain indmv elimclause indclause in
     let branchsigns = compute_construtor_signatures isrec ind in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7484139c68..3038a95068 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -139,7 +139,8 @@ let introduction ?(check=true) id =
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if check && mem_named_context id hyps then
-      error ("Variable " ^ Id.to_string id ^ " is already declared.")
+      errorlabstrm "Tactics.introduction"
+        (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     match kind_of_term (whd_evar sigma concl) with
     | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b
@@ -751,8 +752,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function (e, info) -> match e with
             | RefinerError IntroNeedsProduct ->
-                Proofview.tclZERO 
-		  (Errors.UserError("Intro",str "No product even after head-reduction."))
+                Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
             | e -> Proofview.tclZERO ~info e
           end
   end
@@ -1358,7 +1358,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       | None -> None
   in elim
 
-let descend_in_conjunctions avoid tac exit c =
+let descend_in_conjunctions avoid tac (err, info) c =
   Proofview.Goal.nf_enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -1392,9 +1392,8 @@ let descend_in_conjunctions avoid tac exit c =
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
            end))
-    | None ->
-	raise Exit
-  with RefinerError _|UserError _|Exit -> exit ()
+    | None -> Proofview.tclZERO ~info err
+  with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
   end
 
 (****************************************************)
@@ -1417,7 +1416,15 @@ let solve_remaining_apply_goals =
     with Not_found -> Proofview.tclUNIT ()
   else Proofview.tclUNIT ()
   end
-  
+
+let tclORELSEOPT t k =
+  Proofview.tclORELSE t
+    (fun e -> match k e with
+    | None ->
+      let (e, info) = e in
+      Proofview.tclZERO ~info e
+    | Some tac -> tac)
+
 let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
   Proofview.Goal.nf_enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
@@ -1442,50 +1449,46 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
       with UserError _ as exn ->
         Proofview.tclZERO exn
     in
-    Proofview.tclORELSE
+    let rec try_red_apply thm_ty (exn0, info) =
+      try
+        (* Try to head-reduce the conclusion of the theorem *)
+        let red_thm = try_red_product env sigma thm_ty in
+        tclORELSEOPT
+          (try_apply red_thm concl_nprod)
+          (function (e, info) -> match e with
+          | PretypeError _|RefinerError _|UserError _|Failure _ ->
+            Some (try_red_apply red_thm (exn0, info))
+          | _ -> None)
+      with Redelimination ->
+        (* Last chance: if the head is a variable, apply may try
+            second order unification *)
+        let info = Loc.add_loc info loc in
+        let tac =
+          if with_destruct then
+            descend_in_conjunctions []
+              (fun b id ->
+                Tacticals.New.tclTHEN
+                  (try_main_apply b (mkVar id))
+                  (Proofview.V82.tactic (thin [id])))
+              (exn0, info) c
+          else
+            Proofview.tclZERO ~info exn0 in
+        if not (Int.equal concl_nprod 0) then
+          tclORELSEOPT
+            (try_apply thm_ty 0)
+            (function (e, info) -> match e with
+            | PretypeError _|RefinerError _|UserError _|Failure _->
+              Some tac
+            | _ -> None)
+        else
+          tac
+    in
+    tclORELSEOPT
       (try_apply thm_ty0 concl_nprod)
       (function (e, info) -> match e with
-        | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
-	let rec try_red_apply thm_ty =
-          try 
-            (* Try to head-reduce the conclusion of the theorem *)
-            let red_thm = try_red_product env sigma thm_ty in
-            Proofview.tclORELSE
-              (try_apply red_thm concl_nprod)
-              (function (e, info) -> match e with
-              | PretypeError _|RefinerError _|UserError _|Failure _ ->
-		try_red_apply red_thm
-              | exn -> iraise (exn, info))
-          with Redelimination ->
-            (* Last chance: if the head is a variable, apply may try
-	       second order unification *)
-            let tac =
-	      if with_destruct then
-                descend_in_conjunctions []
-                  (fun b id ->
-                    Tacticals.New.tclTHEN
-                      (try_main_apply b (mkVar id))
-                      (Proofview.V82.tactic (thin [id])))
-                  (fun _ ->
-                    let info = Loc.add_loc info loc in
-                    Proofview.tclZERO ~info exn0) c
-	      else
-                let info = Loc.add_loc info loc in
-		Proofview.tclZERO ~info exn0 in
-            if not (Int.equal concl_nprod 0) then
-              try
-                Proofview.tclORELSE
-                  (try_apply thm_ty 0)
-                  (function (e, info) -> match e with
-                  | PretypeError _|RefinerError _|UserError _|Failure _->
-                    tac
-                  | exn -> iraise (exn, info))
-              with UserError _ | Exit ->
-                tac
-            else
-              tac
-	in try_red_apply thm_ty0
-      | exn -> iraise (exn, info))
+      | PretypeError _|RefinerError _|UserError _|Failure _ ->
+        Some (try_red_apply thm_ty0 (e, info))
+      | _ -> None)
     end
   in
     Tacticals.New.tclTHENLIST [
@@ -1596,10 +1599,10 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
             tac id
           ])
     with e when with_destruct && Errors.noncritical e ->
-      let e = Errors.push e in
+      let (e, info) = Errors.push e in
         (descend_in_conjunctions [targetid]
            (fun b id -> aux (id::idstoclear) b (mkVar id))
-           (fun _ -> iraise e) c)
+           (e, info) c)
     end
   in
   aux [] with_destruct d
@@ -1871,8 +1874,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when not (Int.equal n nconstr) ->
-	error ("Not an inductive goal with "^
-	       string_of_int n ^ String.plural n " constructor"^".")
+	errorlabstrm "Tactics.check_number_of_constructors"
+          (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
   if i > nconstr then error "Not enough constructors."
@@ -3043,7 +3046,7 @@ let make_up_names n ind_opt cname =
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
-  error ("Cannot recognize "^s^"an induction scheme.")
+  errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
 let glob = Universes.constr_of_global
 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index e6f33a47be..59c5792377 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -318,7 +318,7 @@ let tauto_intuitionistic flags =
     (intuition_gen (default_ist ()) flags <:tactic<fail>>)
     begin function (e, info) -> match e with
       | Refiner.FailError _ | UserError _ ->
-          Proofview.tclZERO (UserError ("tauto" , str "tauto failed."))
+          Tacticals.New.tclZEROMSG (str "tauto failed.")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -330,7 +330,7 @@ let tauto_classical flags nnpp =
   Proofview.tclORELSE
     (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
     begin function (e, info) -> match e with
-      | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
+      | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.")
       | e -> Proofview.tclZERO ~info e
     end