Évolutions diverses et variées.

- Correction divers messages d'erreur
  - lorsque rien à réécrire dans une hyp,
  - lorsqu'une variable ltac n'est pas liée,
  - correction anomalie en présence de ?id dans le "as" de induction,
  - correction mauvais env dans message d'erreur de unify_0.

- Diverses extensions et améliorations
  - "specialize" :
    - extension au cas (fun x1 ... xn => H u1 ... un),
    - renommage au même endroit.
  - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
  - "induction"
    - intro des IH toujours au sommet même si induction sur var quantifiée,
    - ajout d'un hack pour la reconnaissance de schémas inductifs comme
      N_ind_double mais il reste du boulot pour reconnaître (et/ou
      réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
      dans l'ordre standard,
    - vérification de longueur et éventuelle complétion des
      intropatterns dans le cas de sous-patterns destructifs dans induction
      (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
       le n dans le contexte),
    - localisation des erreurs d'intropattern,
    - ajout d'un pattern optionnel après "as" pour forcer une égalité et la
      nommer (*).
  - "apply" accepte plusieurs arguments séparés par des virgules (*).
  - Plus de robustesse pour clear en présence d'evars.
  - Amélioration affichage TacFun dans Print Ltac.
  - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
    (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
  - Fusion VTactic/VFun dans l'espoir.
  - Mise en place d'un système de trace de la pile des appels Ltac (tout en
    préservant certains aspects de la récursivité terminale - cf bug #468).

- Tactiques primitives

  - ajout de "move before" dans les tactiques primitives et ajout des
    syntaxes move before et move dependent au niveau utilisateur (*),
  - internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
  - suppression de Intro_replacing et du code sous-traitant

- Nettoyage
  - Suppression cible et fichiers minicoq non portés depuis longtemps.

(*) Extensions de syntaxe qu'il pourrait être opportun de discuter



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 67 insertions, 527 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 9192db7222..b3d76b89b4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -55,6 +55,8 @@ let subst_in_constr (_,subst,(ind,const)) =
 exception EqNotFound of string 
 exception EqUnknown of string
 
+let dl = dummy_loc
+
 (* Some pre declaration of constant we are going to use *)
 let bb = constr_of_global Coqlib.glob_bool
 
@@ -514,13 +516,13 @@ let compute_bl_tact ind lnamesparrec nparrec  =
                      new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
                                         Rawterm.NoBindings))]
                                 None
-                                Genarg.IntroAnonymous
+                                (None,None)
 		                None;
                      intro_using freshm;
                      new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm),
                                     Rawterm.NoBindings))]
                                 None
-                                Genarg.IntroAnonymous
+                                (None,None)
 		                None;
                      intro_using freshz;
                      intros;
@@ -542,9 +544,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                             (new_destruct false [Tacexpr.ElimOnConstr
                                       ((mkVar freshz,Rawterm.NoBindings))]
                                   None
-                                  ( Genarg.IntroOrAndPattern [[
-                                    Genarg.IntroIdentifier fresht;
-                                    Genarg.IntroIdentifier freshz]]) None) gl
+                                  (None, Some (dl,Genarg.IntroOrAndPattern [[
+                                    dl,Genarg.IntroIdentifier fresht;
+                                    dl,Genarg.IntroIdentifier freshz]])) None) gl
                         ]);
 (*
   Ci a1 ... an = Ci b1 ... bn 
@@ -632,13 +634,13 @@ let compute_lb_tact ind lnamesparrec nparrec =
                      new_induct false [Tacexpr.ElimOnConstr 
                                     ((mkVar freshn),Rawterm.NoBindings)] 
                                 None
-                                Genarg.IntroAnonymous
+                                (None,None)
 		                None;
                      intro_using freshm;
                      new_destruct false [Tacexpr.ElimOnConstr 
                                     ((mkVar freshm),Rawterm.NoBindings)]
                                 None
-                                Genarg.IntroAnonymous
+                                (None,None)
 		                None;
                      intro_using freshz;
                      intros;
@@ -746,7 +748,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
       Pfedit.by ( tclTHENSEQ [
                         intros_using fresh_first_intros;
                         intros_using [freshn;freshm];
-                        assert_as true (Genarg.IntroIdentifier freshH) (
+                        assert_as true (dl,Genarg.IntroIdentifier freshH) (
                     mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
                   ) ]); 
 (*we do this so we don't have to prove the same goal twice *)
@@ -754,7 +756,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
                    (new_destruct false [Tacexpr.ElimOnConstr
                                   (eqbnm,Rawterm.NoBindings)]
                                 None
-                                Genarg.IntroAnonymous
+                                (None,None)
 		                None)
                   Auto.default_auto
                 );
@@ -764,9 +766,9 @@ let compute_dec_tact ind lnamesparrec nparrec =
                     new_destruct false [Tacexpr.ElimOnConstr 
                                     ((mkVar freshH),Rawterm.NoBindings)] 
                                 None
-                                (Genarg.IntroOrAndPattern [
-                                    [Genarg.IntroAnonymous];
-                                    [Genarg.IntroIdentifier freshH2]]) None
+                                (None,Some (dl,Genarg.IntroOrAndPattern [
+                                    [dl,Genarg.IntroAnonymous];
+                                    [dl,Genarg.IntroIdentifier freshH2]])) None
       );
       let arfresh = Array.of_list fresh_first_intros in
         let xargs = Array.sub arfresh 0 (2*nparrec) in
@@ -793,7 +795,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
                       unfold_constr (Lazy.force Coqlib.coq_not_ref);
                       intro;
                       Equality.subst_all;
-                assert_as true (Genarg.IntroIdentifier freshH3) 
+                assert_as true (dl,Genarg.IntroIdentifier freshH3) 
                 (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
           ]);
           Pfedit.by 
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index b11592ba48..488c398340 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -40,15 +40,15 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
   | Sys_error msg -> 
       hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
   | UserError(s,pps) -> 
-      hov 1 (str "User error: " ++ where s ++ pps)
+      hov 0 (str "Error: " ++ where s ++ pps)
   | Out_of_memory -> 
       hov 0 (str "Out of memory.")
   | Stack_overflow -> 
       hov 0 (str "Stack overflow.")
   | Anomaly (s,pps) -> 
-      hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ())
+      hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
   | Match_failure(filename,pos1,pos2) ->
-      hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ 
+      hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ 
       if Sys.ocaml_version = "3.06" then
 		   (str " from character " ++ int pos1 ++ 
                     str " to " ++ int pos2)
@@ -83,6 +83,11 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
   | RecursionSchemeError e -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
+  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when s <> mt () ->
+      explain_exn_default_aux anomaly_string report_fn exc
+  | Proof_type.LtacLocated (s,exc) ->
+      hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
+             ++ explain_exn_default_aux anomaly_string report_fn exc)
   | Cases.PatternMatchingError (env,e) -> 
       hov 0
 	(str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
@@ -100,7 +105,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
 	       str "No constant of this name:" ++ spc () ++ 
                Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
-      hov 0 (str "Error: Tactic failure" ++ s ++
+      hov 0 (str "Error: Tactic failure:" ++ s ++
              if i=0 then mt () else str " (level " ++ int i ++ str").")
   | Stdpp.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
deleted file mode 100644
index 91e77f495a..0000000000
--- a/toplevel/fhimsg.ml
+++ /dev/null
@@ -1,355 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Sign
-open Environ
-open Type_errors
-open Reduction
-open G_minicoq
-
-module type Printer = sig
-  val pr_term : path_kind -> env -> constr -> std_ppcmds
-end
-
-module Make = functor (P : Printer) -> struct
-
-  let print_decl k env (s,typ) =
-    let ptyp = P.pr_term k env typ in 
-    (spc () ++ pr_id s ++ str" : " ++ ptyp)
-  
-  let print_binding k env = function
-    | Anonymous,ty -> 
-	(spc () ++ str"_" ++ str" : " ++ P.pr_term k env ty)
-    | Name id,ty -> 
-	(spc () ++ pr_id id ++ str" : " ++ P.pr_term k env ty)
-
-(****
-  let sign_it_with f sign e =
-    snd (fold_named_context
-	   (fun (id,v,t) (sign,e) -> (add_named_decl (id,v,t) sign, f id t sign e))
-           sign (empty_named_context,e))
-
-  let dbenv_it_with f env e =
-    snd (dbenv_it 
-	   (fun na t (env,e) -> (add_rel_decl (na,t) env, f na t env e))
-           env (gLOB(get_globals env),e))
-****)
-      
-  let pr_env k env =
-    let sign_env =
-      fold_named_context
-	(fun env (id,_,t) pps ->
-           let pidt =  print_decl k env (id,t) in (pps ++ fnl () ++ pidt))
-	env (mt ()) 
-    in
-    let db_env =
-      fold_rel_context
-	(fun env (na,_,t) pps ->
-           let pnat = print_binding k env (na,t) in (pps ++ fnl () ++ pnat))
-	env (mt ())
-    in 
-    (sign_env ++ db_env)
-    
-  let pr_ne_ctx header k env =
-    if rel_context env = [] && named_context env = [] then
-      (mt ())
-    else
-      (header ++ pr_env k env)
-
-
-let explain_unbound_rel k ctx n =
-  let pe = pr_ne_ctx (str"in environment") k ctx in
-  (str"Unbound reference: " ++ pe ++ fnl () ++
-     str"The reference " ++ int n ++ str" is free")
-
-let explain_not_type k ctx c =
-  let pe = pr_ne_ctx (str"In environment") k ctx in
-  let pc = P.pr_term k ctx c in
-  (pe ++ cut () ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
-     str"should be typed by Set, Prop or Type.");;
-
-let explain_bad_assumption k ctx c =
-  let pc = P.pr_term k ctx c in
-  (str "Cannot declare a variable or hypothesis over the term" ++
-     brk(1,1) ++ pc ++ spc () ++ str "because this term is not a type.");;
-
-let explain_reference_variables id =
-  (str "the constant" ++ spc () ++ pr_id id ++ spc () ++ 
-     str "refers to variables which are not in the context")
-
-let msg_bad_elimination ctx k = function
-  | Some(ki,kp,explanation) ->
-      let pki = P.pr_term k ctx ki in
-      let pkp = P.pr_term k ctx kp in
-      (hov 0 
-         (fnl () ++ str "Elimination of an inductive object of sort : " ++
-            pki ++ brk(1,0) ++
-            str "is not allowed on a predicate in sort : " ++ pkp ++fnl () ++
-            str "because" ++ spc () ++ str explanation))
-  | None -> 
-      (mt ())
-
-let explain_elim_arity k ctx ind aritylst c pj okinds = 
-  let pi = P.pr_term k ctx ind in
-  let ppar = prlist_with_sep pr_coma (P.pr_term k ctx) aritylst in
-  let pc = P.pr_term k ctx c in
-  let pp = P.pr_term k ctx pj.uj_val in
-  let ppt = P.pr_term k ctx pj.uj_type in
-  (str "Incorrect elimination of" ++ brk(1,1) ++ pc ++ spc () ++
-     str "in the inductive type" ++ brk(1,1) ++ pi ++ fnl () ++
-     str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++
-     str "has type" ++ brk(1,1) ++ ppt ++ fnl () ++
-     str "It should be one of :" ++ brk(1,1) ++ hov 0 ppar ++ fnl () ++
-     msg_bad_elimination ctx k okinds)
-
-let explain_case_not_inductive k ctx cj =
-  let pc = P.pr_term k ctx cj.uj_val in
-  let pct = P.pr_term k ctx cj.uj_type in
-  (str "In Cases expression" ++ brk(1,1) ++ pc ++ spc () ++ 
-     str "has type" ++ brk(1,1) ++ pct ++ spc () ++ 
-     str "which is not an inductive definition")
-  
-let explain_number_branches k ctx cj expn =
-  let pc = P.pr_term k ctx cj.uj_val in
-  let pct = P.pr_term k ctx cj.uj_val in
-  (str "Cases on term" ++ brk(1,1) ++ pc ++ spc () ++
-     str "of type" ++ brk(1,1) ++ pct ++ spc () ++
-     str "expects " ++  int expn ++ str " branches")
-
-let explain_ill_formed_branch k ctx c i actty expty =
-  let pc = P.pr_term k ctx c in
-  let pa = P.pr_term k ctx actty in
-  let pe = P.pr_term k ctx expty in
-  (str "In Cases expression on term" ++ brk(1,1) ++ pc ++
-     spc () ++ str "the branch " ++ int (i+1) ++
-     str " has type" ++ brk(1,1) ++ pa ++ spc () ++ 
-     str "which should be:" ++ brk(1,1) ++ pe)
-
-let explain_generalization k ctx (name,var) c =
-  let pe = pr_ne_ctx (str"in environment") k ctx in
-  let pv = P.pr_term k ctx var in
-  let pc = P.pr_term k (push_rel (name,None,var) ctx) c in
-  (str"Illegal generalization: " ++ pe ++ fnl () ++
-     str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
-     str"over" ++ brk(1,1) ++ pc ++ spc () ++
-     str"which should be typed by Set, Prop or Type.")
-
-let explain_actual_type k ctx c ct pt =
-  let pe = pr_ne_ctx (str"In environment") k ctx in
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
-  let pt = P.pr_term k ctx pt in
-  (pe ++ fnl () ++
-     str"The term" ++ brk(1,1) ++ pc ++ spc () ++
-     str"does not have type" ++ brk(1,1) ++ pt ++ fnl () ++
-     str"Actually, it has type" ++ brk(1,1) ++ pct)
-
-let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
-  let ctx = make_all_name_different ctx in
-  let pe = pr_ne_ctx (str"in environment") k ctx in
-  let pr = pr_term k ctx rator.uj_val in
-  let prt = pr_term k ctx rator.uj_type in
-  let term_string = if List.length randl > 1 then "terms" else "term" in
-  let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
-  let appl = prlist_with_sep pr_fnl 
-	       (fun c ->
-		  let pc = pr_term k ctx c.uj_val in
-		  let pct = pr_term k ctx c.uj_type in
-		  hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
-  in
-  (str"Illegal application (Type Error): " ++ pe ++ fnl () ++
-     str"The term" ++ brk(1,1) ++ pr ++ spc () ++
-     str"of type" ++ brk(1,1) ++ prt ++ spc () ++
-     str("cannot be applied to the "^term_string) ++ fnl () ++ 
-     str" " ++ v 0 appl ++ fnl () ++
-     str"The " ++int n ++ str (many^" term of type ") ++
-     pr_term k ctx actualtyp ++
-     str" should be of type " ++ pr_term k ctx exptyp)
-
-let explain_cant_apply_not_functional k ctx rator randl =
-  let ctx = make_all_name_different ctx in
-  let pe = pr_ne_ctx (str"in environment") k ctx in
-  let pr = pr_term k ctx rator.uj_val in
-  let prt = pr_term k ctx rator.uj_type in
-  let term_string = if List.length randl > 1 then "terms" else "term" in
-  let appl = prlist_with_sep pr_fnl 
-	       (fun c ->
-		  let pc = pr_term k ctx c.uj_val in
-		  let pct = pr_term k ctx c.uj_type in
-		  hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
-  in
-  (str"Illegal application (Non-functional construction): " ++ pe ++ fnl () ++
-     str"The term" ++ brk(1,1) ++ pr ++ spc () ++
-     str"of type" ++ brk(1,1) ++ prt ++ spc () ++
-     str("cannot be applied to the "^term_string) ++ fnl () ++ 
-     str" " ++ v 0 appl ++ fnl ())
-
-(* (co)fixpoints *)
-let explain_ill_formed_rec_body k ctx err names i vdefs =
-  let str = match err with
-
-  (* Fixpoint guard errors *)
-  | NotEnoughAbstractionInFixBody ->
-      (str "Not enough abstractions in the definition")
-  | RecursionNotOnInductiveType ->
-      (str "Recursive definition on a non inductive type")
-  | RecursionOnIllegalTerm ->
-      (str "Recursive call applied to an illegal term")
-  | NotEnoughArgumentsForFixCall ->
-      (str "Not enough arguments for the recursive call")
-
-  (* CoFixpoint guard errors *)
-  (* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
-  | CodomainNotInductiveType c ->
-      (str "The codomain is" ++ spc () ++ P.pr_term k ctx c ++ spc () ++
-	 str "which should be a coinductive type")
-  | NestedRecursiveOccurrences ->
-      (str "Nested recursive occurrences")
-  | UnguardedRecursiveCall c ->
-      (str "Unguarded recursive call")
-  | RecCallInTypeOfAbstraction c ->
-      (str "Not allowed recursive call in the domain of an abstraction")
-  | RecCallInNonRecArgOfConstructor c ->
-      (str "Not allowed recursive call in a non-recursive argument of constructor")
-  | RecCallInTypeOfDef c ->
-      (str "Not allowed recursive call in the type of a recursive definition")
-  | RecCallInCaseFun c ->
-      (str "Not allowed recursive call in a branch of cases")
-  | RecCallInCaseArg c -> 
-      (str "Not allowed recursive call in the argument of cases")
-  | RecCallInCasePred c ->
-      (str "Not allowed recursive call in the type of cases in")
-  | NotGuardedForm c ->
-      str "Sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++
-      str "not in guarded form (should be a constructor, Cases or CoFix)"
-in
-  let pvd = P.pr_term k ctx vdefs.(i) in
-  let s =
-    match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in
-  (str ++ fnl () ++ str"The " ++
-     if Array.length vdefs = 1 then (mt ()) else (int (i+1) ++ str "-th ") ++
-     str"recursive definition" ++ spc () ++ str s ++
-	 spc () ++ str":=" ++ spc () ++ pvd ++ spc () ++
-     str "is not well-formed")
-    
-let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
-  let pvd = P.pr_term k ctx (vdefj.(i)).uj_val in
-  let pvdt = P.pr_term k ctx (vdefj.(i)).uj_type in
-  let pv = P.pr_term k ctx vargs.(i) in
-  (str"The " ++
-     if Array.length vdefj = 1 then (mt ()) else (int (i+1) ++ str "-th") ++
-     str"recursive definition" ++ spc () ++ pvd ++ spc () ++
-     str "has type" ++ spc () ++ pvdt ++spc () ++ str "it should be" ++ spc () ++ pv)
-
-let explain_not_inductive k ctx c =
-  let pc = P.pr_term k ctx c in
-  (str"The term" ++ brk(1,1) ++ pc ++ spc () ++
-     str "is not an inductive definition")
-
-let explain_ml_case k ctx mes c ct br brt =
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
-  let expln =
-    match mes with
-      | "Inductive" -> (pct ++ str "is not an inductive definition")
-      | "Predicate" -> (str "ML case not allowed on a predicate")
-      | "Absurd" -> (str "Ill-formed case expression on an empty type")
-      | "Decomp" ->
-          let plf = P.pr_term k ctx br in
-          let pft = P.pr_term k ctx brt in
-          (str "The branch " ++ plf ++ ws 1 ++ cut () ++ str "has type " ++ pft ++
-             ws 1 ++ cut () ++
-             str "does not correspond to the inductive definition")
-      | "Dependent" ->
-          (str "ML case not allowed for a dependent case elimination")
-      | _ -> (mt ())
-  in
-  hov 0 (str "In ML case expression on " ++ pc ++ ws 1 ++ cut () ++
-           str "of type" ++  ws 1 ++ pct ++ ws 1 ++ cut () ++ 
-           str "which is an inductive predicate." ++ fnl () ++ expln)
-
-let explain_type_error k ctx = function
-  | UnboundRel n -> 
-      explain_unbound_rel k ctx n
-  | NotAType c -> 
-      explain_not_type k ctx c.uj_val
-  | BadAssumption c -> 
-      explain_bad_assumption k ctx c
-  | ReferenceVariables id -> 
-      explain_reference_variables id
-  | ElimArity (ind, aritylst, c, pj, okinds) ->
-      explain_elim_arity k ctx (mkMutInd ind) aritylst c pj okinds 
-  | CaseNotInductive cj -> 
-      explain_case_not_inductive k ctx cj
-  | NumberBranches (cj, n) -> 
-      explain_number_branches k ctx cj n
-  | IllFormedBranch (c, i, actty, expty) -> 
-      explain_ill_formed_branch k ctx c i actty expty 
-  | Generalization (nvar, c) ->
-      explain_generalization k ctx nvar c.uj_val
-  | ActualType (c, ct, pt) -> 
-      explain_actual_type k ctx c ct pt
-  | CantApplyBadType (s, rator, randl) ->
-      explain_cant_apply_bad_type k ctx s rator randl
-  | CantApplyNonFunctional (rator, randl) ->
-      explain_cant_apply_not_functional k ctx rator randl
-  | IllFormedRecBody (i, lna, vdefj, vargs) ->
-      explain_ill_formed_rec_body k ctx i lna vdefj vargs
-  | IllTypedRecBody (i, lna, vdefj, vargs) ->
-      explain_ill_typed_rec_body k ctx i lna vdefj vargs
-(*
-  | NotInductive c ->
-      explain_not_inductive k ctx c
-  | MLCase (mes,c,ct,br,brt) ->
-      explain_ml_case k ctx mes c ct br brt
-*)
-  | _ -> 
-      (str "Unknown type error (TODO)")
-
-let explain_refiner_bad_type k ctx arg ty conclty =
-  errorlabstrm "Logic.conv_leq_goal"
-    (str"refiner was given an argument" ++ brk(1,1) ++ 
-       P.pr_term k ctx arg ++ spc () ++
-       str"of type" ++ brk(1,1) ++ P.pr_term k ctx ty ++ spc () ++
-       str"instead of" ++ brk(1,1) ++ P.pr_term k ctx conclty)
-
-let explain_refiner_occur_meta k ctx t =
-  errorlabstrm "Logic.mk_refgoals"
-    (str"cannot refine with term" ++ brk(1,1) ++ P.pr_term k ctx t ++
-       spc () ++ str"because there are metavariables, and it is" ++
-       spc () ++ str"neither an application nor a Case")
-
-let explain_refiner_cannot_applt k ctx t harg =
-  errorlabstrm "Logic.mkARGGOALS"
-    (str"in refiner, a term of type " ++ brk(1,1) ++
-       P.pr_term k ctx t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
-       P.pr_term k ctx harg)
-
-let explain_occur_check k ctx ev rhs =
-  let id = "?" ^ string_of_int ev in
-  let pt = P.pr_term k ctx rhs in
-  errorlabstrm "Trad.occur_check"
-    (str"Occur check failed: tried to define " ++ str id ++
-      str" with term" ++ brk(1,1) ++ pt)
-
-let explain_not_clean k ctx sp t =
-  let c = mkRel (Intset.choose (free_rels t)) in
-  let id = string_of_id (Names.basename sp) in
-  let var = P.pr_term k ctx c in
-  errorlabstrm "Trad.not_clean"
-    (str"Tried to define " ++ str id ++
-       str" with a term using variable " ++ var ++ spc () ++
-       str"which is not in its scope.")
-
-end
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 10f8e39c3a..422555d047 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -424,12 +424,9 @@ let explain_cannot_unify_binding_type env m n =
   str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
 
 let explain_cannot_find_well_typed_abstraction env p l =
-  let la,lc = list_chop (List.length l - 1) l in
   str "Abstracting over the " ++
   str (plural (List.length l) "term") ++ spc () ++ 
-  hov 0 (prlist_with_sep pr_coma (pr_lconstr_env env) la ++
-         (if la<>[] then str " and" ++ spc () else mt()) ++ 
-         pr_lconstr_env env (List.hd lc)) ++ spc () ++
+  hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++
   str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ 
   str "which is ill-typed."
 
@@ -561,7 +558,7 @@ let explain_refiner_unresolved_bindings l =
   prlist_with_sep pr_coma pr_name l ++ str"."
 
 let explain_refiner_cannot_apply t harg =
-  str "In refiner, a term of type " ++ brk(1,1) ++
+  str "In refiner, a term of type" ++ brk(1,1) ++
   pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
   pr_lconstr harg ++ str "."
 
@@ -784,3 +781,40 @@ let explain_reduction_tactic_error = function
       str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' e
+
+let explain_ltac_call_trace (last,trace,loc) =
+  let calls = last :: List.rev (List.map snd trace) in
+  let pr_call = function
+  | Proof_type.LtacNotationCall s -> quote (str s)
+  | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+  | Proof_type.LtacVarCall (id,t) ->
+      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ 
+      Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+  | Proof_type.LtacAtomCall (te,otac) -> quote
+      (Pptactic.pr_glob_tactic (Global.env())
+	(Tacexpr.TacAtom (dummy_loc,te)))
+      ++ (match !otac with
+      | Some te' when (Obj.magic te' <> te) ->
+	  strbrk " (expanded to " ++ quote
+	  (Pptactic.pr_tactic (Global.env())
+	    (Tacexpr.TacAtom (dummy_loc,te')))
+	++ str ")"
+      | _ -> mt ())
+  | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
+      let filter =
+	function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in
+      let unboundvars = list_map_filter filter unboundvars in
+      quote (pr_rawconstr_env (Global.env()) c) ++
+      (if unboundvars <> [] or vars <> [] then
+	strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) -> 
+	pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
+	  (List.rev vars @ unboundvars)
+       else mt()) ++ str ")" in
+  if calls <> [] then
+    let kind_of_last_call = match list_last calls with
+    | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
+    | _ -> ", last call failed." in
+    hov 0 (str "In nested Ltac calls to " ++ 
+           pr_enum pr_call calls ++ strbrk kind_of_last_call)
+  else
+    mt ()
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index d7a72bedee..053bf16a3b 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -40,3 +40,6 @@ val explain_pattern_matching_error :
 
 val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
+
+val explain_ltac_call_trace : 
+  Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc -> std_ppcmds
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
deleted file mode 100644
index e22b33e24c..0000000000
--- a/toplevel/minicoq.ml
+++ /dev/null
@@ -1,149 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Sign
-open Declarations
-open Inductive
-open Type_errors
-open Safe_typing
-open G_minicoq
-
-let (env : safe_environment ref) = ref empty_environment
-
-let locals () =
-  List.map (fun (id,b,t) -> (id, make_path [] id CCI))
-    (named_context !env)
-
-let lookup_named id =
-  let rec look n = function
-    | [] -> mkVar id
-    | (Name id')::_ when id = id' -> mkRel n
-    | _::r -> look (succ n) r
-  in
-  look 1
-
-let args sign = Array.of_list (instance_from_section_context sign)
-
-let rec globalize bv c = match kind_of_term c with
-  | Var id -> lookup_named id bv
-  | Const (sp, _) ->
-      let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps)
-  | Ind (sp,_ as spi, _) ->
-      let mib = lookup_mind sp !env in mkMutInd (spi, args mib.mind_hyps)
-  | Construct ((sp,_),_ as spc, _) ->
-      let mib = lookup_mind sp !env in mkMutConstruct (spc, args mib.mind_hyps)
-  | _ -> map_constr_with_named_binders (fun na l -> na::l) globalize bv c
-
-let check c = 
-  let c = globalize [] c in
-  let (j,u) = safe_infer !env c in
-  let ty = j_type j in
-  let pty = pr_term CCI (env_of_safe_env !env) ty in
-  mSGNL (hov 0 (str"  :" ++ spc () ++ hov 0 pty ++ fnl ()))
-
-let definition id ty c =
-  let c = globalize [] c in
-  let ty = Option.map (globalize []) ty in
-  let ce = { const_entry_body = c; const_entry_type = ty } in
-  let sp = make_path [] id CCI in
-  env := add_constant sp ce (locals()) !env;
-  mSGNL (hov 0 (pr_id id ++ spc () ++ str"is defined" ++ fnl ()))
-
-let parameter id t =
-  let t = globalize [] t in
-  let sp = make_path [] id CCI in
-  env := add_parameter sp t (locals()) !env;
-  mSGNL (hov 0 (str"parameter" ++ spc () ++ pr_id id ++ 
-		  spc () ++ str"is declared" ++ fnl ()))
-
-let variable id t =
-  let t = globalize [] t in
-  env := push_named_assum (id,t) !env;
-  mSGNL (hov 0 (str"variable" ++ spc () ++ pr_id id ++ 
-		  spc () ++ str"is declared" ++ fnl ()))
-
-let inductive par inds =
-  let nparams = List.length par in
-  let bvpar = List.rev (List.map (fun (id,_) -> Name id) par) in
-  let name_inds = List.map (fun (id,_,_) -> Name id) inds in
-  let bv = bvpar @  List.rev name_inds in
-  let npar = List.map (fun (id,c) -> (Name id, globalize [] c)) par in
-  let one_inductive (id,ar,cl) =
-    let cv = List.map (fun (_,c) -> prod_it (globalize bv c) npar) cl in
-    { mind_entry_nparams = nparams;
-      mind_entry_params = List.map (fun (id,c) -> (id, LocalAssum c)) par;
-      mind_entry_typename = id;
-      mind_entry_arity = prod_it (globalize bvpar ar) npar;
-      mind_entry_consnames = List.map fst cl;
-      mind_entry_lc = cv }
-  in
-  let inds = List.map one_inductive inds in
-  let mie = { 
-    mind_entry_finite = true;
-    mind_entry_inds = inds }
-  in
-  let sp =
-    let mi1 = List.hd inds in
-    make_path [] mi1.mind_entry_typename CCI in
-  env := add_mind sp mie (locals()) !env;
-  mSGNL (hov 0 (str"inductive type(s) are declared" ++ fnl ()))
-
-
-let execute = function
-  | Check c -> check c
-  | Definition (id, ty, c) -> definition id ty c
-  | Parameter (id, t) -> parameter id t
-  | Variable (id, t) -> variable id t
-  | Inductive (par,inds) -> inductive par inds
-
-let parse_file f =
-  let c = open_in f in
-  let cs = Stream.of_channel c in
-  try
-    while true do
-      let c = Grammar.Entry.parse command cs in execute c
-    done
-  with 
-    | End_of_file | Stdpp.Exc_located (_, End_of_file) -> close_in c; exit 0
-    | exn -> close_in c; raise exn
-
-module Explain = Fhimsg.Make(struct let pr_term = pr_term end)
-
-let rec explain_exn = function
-  | TypeError (k,ctx,te) -> 
-      mSGNL (hov 0 (str "type error:" ++ spc () ++ 
-		      Explain.explain_type_error k ctx te ++ fnl ()))
-  | Stdpp.Exc_located (_,exn) -> 
-      explain_exn exn
-  | exn -> 
-      mSGNL (hov 0 (str"error: " ++ str (Printexc.to_string exn) ++ fnl ()))
-
-let top () =
-  let cs = Stream.of_channel stdin in
-  while true do
-    try
-      let c = Grammar.Entry.parse command cs in execute c
-    with 
-      | End_of_file | Stdpp.Exc_located (_, End_of_file) -> exit 0
-      | exn -> explain_exn exn
-  done
-
-let main () =
-  if Array.length Sys.argv = 1 then
-    parse_file "test"
-  else
-    if Sys.argv.(1) = "-top" then top () else parse_file (Sys.argv.(1))
-
-let _ = Printexc.print main ()
-
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ae91628600..399c18c921 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1256,7 +1256,7 @@ let vernac_check_guard () =
 	pfterm; 
       (str "The condition holds up to here")
     with UserError(_,s) -> 
-      (str ("Condition violated : ") ++s)
+      (str ("Condition violated: ") ++s)
   in 
   msgnl message