É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

13 files changed, 257 insertions, 392 deletions

diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
deleted file mode 100644
index fe7906f63d..0000000000
--- a/parsing/g_minicoq.ml4
+++ /dev/null
@@ -1,177 +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        *)
-(************************************************************************)
-
-(*i camlp4use: "pa_extend.cmo" i*)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Univ
-open Term
-open Environ
-
-let lexer =
-  {Token.func = Lexer.func; Token.using = Lexer.add_token;
-   Token.removing = (fun _ -> ()); Token.tparse = Lexer.tparse;
-   Token.text = Lexer.token_text}
-;;
-
-type command =
-  | Definition of identifier * constr option * constr
-  | Parameter of identifier * constr
-  | Variable of identifier * constr
-  | Inductive of 
-      (identifier * constr) list *
-      (identifier * constr * (identifier * constr) list) list
-  | Check of constr
-
-let gram = Grammar.create lexer
-
-let term = Grammar.Entry.create gram "term"
-let name = Grammar.Entry.create gram "name"
-let nametype = Grammar.Entry.create gram "nametype"
-let inductive = Grammar.Entry.create gram "inductive"
-let constructor = Grammar.Entry.create gram "constructor"
-let command = Grammar.Entry.create gram "command"
-
-let path_of_string s = make_path [] (id_of_string s)
-
-EXTEND
-  name: 
-  [ [ id = IDENT -> Name (id_of_string id)
-    | "_" -> Anonymous
-  ] ];
-  nametype: 
-  [ [ id = IDENT; ":"; t = term -> (id_of_string id, t) 
-  ] ];
-  term: 
-  [ [ id = IDENT -> 
-	mkVar (id_of_string id) 
-    | IDENT "Rel"; n = INT ->
-	mkRel (int_of_string n)
-    | "Set" ->
-	mkSet
-    | "Prop" ->
-	mkProp
-    | "Type" ->
-	mkType (new_univ())
-    | "Const"; id = IDENT ->
-	mkConst (path_of_string id, [||])
-    | "Ind"; id = IDENT; n = INT ->
-	let n = int_of_string n in
-	mkMutInd ((path_of_string id, n), [||])
-    | "Construct"; id = IDENT; n = INT; i = INT ->
-	let n = int_of_string n and i = int_of_string i in
-	mkMutConstruct (((path_of_string id, n), i), [||])
-    | "["; na = name; ":"; t = term; "]"; c = term ->
-	mkLambda (na,t,c)
-    | "("; na = name; ":"; t = term; ")"; c = term ->
-	mkProd (na,t,c)
-    | c1 = term; "->"; c2 = term ->
-	mkArrow c1 c2
-    | "("; id = IDENT; cl = LIST1 term; ")" ->
-	let c = mkVar (id_of_string id) in
-	mkApp (c, Array.of_list cl)
-    | "("; cl = LIST1 term; ")" ->
-	begin match cl with
-	  | [c] -> c
-	  | c::cl -> mkApp (c, Array.of_list cl)
-	end
-    | "("; c = term; "::"; t = term; ")" ->
-	mkCast (c, t)
-    | "<"; p = term; ">"; 
-	IDENT "Case"; c = term; ":"; "Ind"; id = IDENT; i = INT;
-	"of"; bl = LIST0 term; "end" ->
-	  let ind = (path_of_string id,int_of_string i) in
-	  let nc = List.length bl in
-	  let dummy_pats = Array.create nc RegularPat in
-	  let dummy_ci = [||],(ind,[||],nc,None,dummy_pats) in
-	  mkMutCase (dummy_ci, p, c, Array.of_list bl)
-  ] ];
-  command: 
-  [ [ "Definition"; id = IDENT; ":="; c = term; "." ->
-	Definition (id_of_string id, None, c)
-    | "Definition"; id = IDENT; ":"; t = term; ":="; c = term; "." ->
-	Definition (id_of_string id, Some t, c)
-    | "Parameter"; id = IDENT; ":"; t = term; "." ->
-	Parameter (id_of_string id, t)
-    | "Variable"; id = IDENT; ":"; t = term; "." ->
-	Variable (id_of_string id, t)
-    | "Inductive"; "["; params = LIST0 nametype SEP ";"; "]"; 
-      inds = LIST1 inductive SEP "with" ->
-	Inductive (params, inds)
-    | IDENT "Check"; c = term; "." ->
-	Check c
-    | EOI -> raise End_of_file
-  ] ];
-  inductive: 
-  [ [ id = IDENT; ":"; ar = term; ":="; constrs = LIST0 constructor SEP "|" ->
-        (id_of_string id,ar,constrs)
-  ] ];
-  constructor:
-  [ [ id = IDENT; ":"; c = term -> (id_of_string id,c) ] ];
-END
-
-(* Pretty-print. *)
-
-let print_univers = ref false
-let print_casts = ref false
-
-let print_type u =
-  if !print_univers then (str "Type" ++ pr_uni u)
-  else (str "Type")
-
-let print_name = function
-  | Anonymous -> (str "_")
-  | Name id -> pr_id id
-
-let print_rel bv n = print_name (List.nth bv (pred n))
-
-let rename bv = function
-  | Anonymous -> Anonymous
-  | Name id as na -> 
-      let idl = 
-	List.fold_left 
-	  (fun l n -> match n with Name x -> x::l | _ -> l) [] bv 
-      in
-      if List.mem na bv then Name (next_ident_away id idl) else na
-
-let rec pp bv t =
-  match kind_of_term t with
-  | Sort (Prop Pos) -> (str "Set")
-  | Sort (Prop Null) -> (str "Prop")
-  | Sort (Type u) -> print_type u
-  | Lambda (na, t, c) ->
-      (str"[" ++ print_name na ++ str":" ++ pp bv t ++ str"]" ++ pp (na::bv) c)
-  | Prod (Anonymous, t, c) ->
-      (pp bv t ++ str"->" ++ pp (Anonymous::bv) c)
-  | Prod (na, t, c) ->
-      (str"(" ++ print_name na ++ str":" ++ pp bv t ++ str")" ++ pp (na::bv) c)
-  | Cast (c, t) ->
-      if !print_casts then 
-	(str"(" ++ pp bv c ++ str"::" ++ pp bv t ++ str")")
-      else 
-	pp bv c
-  | App(h, v) ->
-      (str"(" ++ pp bv h ++ spc () ++
-         prvect_with_sep (fun () -> (spc ())) (pp bv) v ++ str")")
-  | Const (sp, _) ->
-      (str"Const " ++ pr_id (basename sp))
-  | Ind ((sp,i), _) ->
-      (str"Ind " ++ pr_id (basename sp) ++ str" " ++ int i)
-  | Construct (((sp,i),j), _) ->
-      (str"Construct " ++ pr_id (basename sp) ++ str" " ++ int i ++ 
-	 str" " ++ int j)
-  | Var id -> pr_id id
-  | Rel n -> print_rel bv n
-  | _ -> (str"<???>")
-
-let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx [])
-
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 092dc9f884..ed8422b109 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -26,7 +26,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
 
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
-let lpar_id_coloneq =
+let test_lpar_id_coloneq =
   Gram.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
       match Stream.npeek 1 strm with
@@ -34,9 +34,7 @@ let lpar_id_coloneq =
             (match Stream.npeek 2 strm with
               | [_; ("IDENT",s)] ->
                   (match Stream.npeek 3 strm with
-	            | [_; _; ("", ":=")] ->
-                        Stream.junk strm; Stream.junk strm; Stream.junk strm;
-                        Names.id_of_string s
+	            | [_; _; ("", ":=")] -> ()
 	            | _ -> raise Stream.Failure)
 	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
@@ -56,7 +54,7 @@ let test_lpar_idnum_coloneq =
         | _ -> raise Stream.Failure)
 
 (* idem for (x:t) *)
-let lpar_id_colon =
+let test_lpar_id_colon =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       match Stream.npeek 1 strm with
@@ -64,9 +62,7 @@ let lpar_id_colon =
             (match Stream.npeek 2 strm with
               | [_; ("IDENT",id)] ->
                   (match Stream.npeek 3 strm with
-                    | [_; _; ("", ":")] ->
-                        Stream.junk strm; Stream.junk strm; Stream.junk strm;
-                        Names.id_of_string id
+                    | [_; _; ("", ":")] -> ()
                     | _ -> raise Stream.Failure)
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
@@ -162,6 +158,8 @@ let mkCLambdaN_simple bl c =
     let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in
     mkCLambdaN_simple_loc loc bl c
 
+let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
+
 let map_int_or_var f = function
   | Rawterm.ArgArg x -> Rawterm.ArgArg (f x)
   | Rawterm.ArgVar _ as y -> y
@@ -237,27 +235,32 @@ GEXTEND Gram
   intropatterns:
     [ [ l = LIST0 simple_intropattern -> l ]]
   ;
-  simple_intropattern:
-    [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
-      | "()" -> IntroOrAndPattern [[]]
-      | "("; si = simple_intropattern; ")" -> IntroOrAndPattern [[si]]
+  disjunctive_intropattern:
+    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> loc,IntroOrAndPattern tc
+      | "()" -> loc,IntroOrAndPattern [[]]
+      | "("; si = simple_intropattern; ")" -> loc,IntroOrAndPattern [[si]]
       | "("; si = simple_intropattern; ","; 
              tc = LIST1 simple_intropattern SEP "," ; ")" -> 
-	       IntroOrAndPattern [si::tc]
+	       loc,IntroOrAndPattern [si::tc]
       | "("; si = simple_intropattern; "&"; 
 	     tc = LIST1 simple_intropattern SEP "&" ; ")" -> 
 	  (* (A & B & C) is translated into (A,(B,C)) *)
 	  let rec pairify = function 
 	    | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
-	    | t::q -> IntroOrAndPattern [[t;pairify q]]
-	  in pairify (si::tc)
-      | "_" -> IntroWildcard loc
-      | prefix = pattern_ident -> IntroFresh prefix
-      | "?" -> IntroAnonymous
-      | id = ident -> IntroIdentifier id
-      | "->" -> IntroRewrite true
-      | "<-" -> IntroRewrite false
-      ] ]
+	    | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]]
+	  in loc,pairify (si::tc) ] ]
+  ;
+  naming_intropattern:
+    [ [ prefix = pattern_ident -> loc, IntroFresh prefix
+      | "?" -> loc, IntroAnonymous
+      | id = ident -> loc, IntroIdentifier id ] ]
+  ;
+  simple_intropattern:
+    [ [ pat = disjunctive_intropattern -> pat
+      | pat = naming_intropattern -> pat
+      | "_" -> loc, IntroWildcard
+      | "->" -> loc, IntroRewrite true
+      | "<-" -> loc, IntroRewrite false ] ]
   ;
   simple_binding:
     [ [ "("; id = ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c)
@@ -402,7 +405,18 @@ GEXTEND Gram
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
   with_names:
-    [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ]
+    [ [ "as"; ipat = simple_intropattern -> ipat
+      | -> dummy_loc,IntroAnonymous ] ]
+  ;
+  with_inversion_names:
+    [ [ "as"; ipat = disjunctive_intropattern -> Some ipat
+      | -> None ] ]
+  ;
+  with_induction_names:
+    [ [ "as"; eq = OPT naming_intropattern; ipat = disjunctive_intropattern
+        -> (eq,Some ipat)
+      | "as"; eq = naming_intropattern -> (Some eq,None)
+      | -> (None,None) ] ]
   ;
   as_name:
     [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
@@ -439,30 +453,40 @@ GEXTEND Gram
   oriented_rewriter : 
     [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
   ; 
+  induction_clause:
+    [ [ lc = LIST1 induction_arg; ipats = with_induction_names; 
+        el = OPT eliminator; cl = opt_clause -> (lc,el,ipats,cl) ] ]
+  ;
+  move_location:
+    [ [ IDENT "after"; id = id_or_meta -> MoveAfter id
+      | IDENT "before"; id = id_or_meta -> MoveBefore id
+      | "at"; IDENT "bottom" -> MoveToEnd true
+      | "at"; IDENT "top" -> MoveToEnd false ] ]
+  ;
   simple_tactic:
     [ [ 
       (* Basic tactics *)
         IDENT "intros"; IDENT "until"; id = quantified_hypothesis -> 
 	  TacIntrosUntil id
       | IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
-      | IDENT "intro"; id = ident; IDENT "after"; id2 = identref ->
-	  TacIntroMove (Some id, Some id2)
-      | IDENT "intro"; IDENT "after"; id2 = identref ->
-	  TacIntroMove (None, Some id2)
-      | IDENT "intro"; id = ident -> TacIntroMove (Some id, None)
-      | IDENT "intro" -> TacIntroMove (None, None)
+      | IDENT "intro"; id = ident; hto = move_location ->
+	  TacIntroMove (Some id, hto)
+      | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto)
+      | IDENT "intro"; id = ident -> TacIntroMove (Some id, no_move)
+      | IDENT "intro" -> TacIntroMove (None, no_move)
 
       | IDENT "assumption" -> TacAssumption
       | IDENT "exact"; c = constr -> TacExact c
       | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
       | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
 
-      | IDENT "apply"; cl = constr_with_bindings -> TacApply (true,false,cl)
-      | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,true,cl)
-      | IDENT "simple"; IDENT "apply"; cl = constr_with_bindings -> 
-          TacApply (false,false,cl)
-      | IDENT "simple"; IDENT "eapply"; cl = constr_with_bindings -> 
-          TacApply (false, true,cl)
+      | IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," ->
+	  TacApply (true,false,cl)
+      | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," ->
+          TacApply (true,true,cl)
+      | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," 
+          -> TacApply (false,false,cl)
+      | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ","           -> TacApply (false,true,cl)
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (false,cl,el)
       | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
@@ -492,10 +516,12 @@ GEXTEND Gram
           TacLetTac (na,c,p,false)
 
       (* Begin compatibility *)
-      | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> 
-	  TacAssert (None,IntroIdentifier id,c)
-      | IDENT "assert"; id = lpar_id_colon; c = lconstr; ")"; tac=by_tactic -> 
-	  TacAssert (Some tac,IntroIdentifier id,c)
+      | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; 
+	  c = lconstr; ")" -> 
+	  TacAssert (None,(loc,IntroIdentifier id),c)
+      | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; 
+	  c = lconstr; ")"; tac=by_tactic -> 
+	  TacAssert (Some tac,(loc,IntroIdentifier id),c)
       (* End compatibility *)
 
       | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic ->
@@ -521,23 +547,19 @@ GEXTEND Gram
 
       (* Derived basic tactics *)
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
-          TacSimpleInduction h
-      | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator; cl = opt_clause -> 
-	    TacNewInduction (false,lc,el,ids,cl)
-      | IDENT "einduction"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator; cl = opt_clause ->
-	    TacNewInduction (true,lc,el,ids,cl)
+          TacSimpleInductionDestruct (true,h)
+      | IDENT "induction"; ic = induction_clause ->
+	  TacInductionDestruct (true,false,[ic])
+      | IDENT "einduction"; ic = induction_clause ->
+	  TacInductionDestruct(true,true,[ic])
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
-          TacSimpleDestruct h
-      | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator; cl = opt_clause ->
-	    TacNewDestruct (false,lc,el,ids,cl)
-      | IDENT "edestruct"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator; cl = opt_clause ->
-	    TacNewDestruct (true,lc,el,ids,cl)
+          TacSimpleInductionDestruct (false,h)
+      | IDENT "destruct"; ic = induction_clause ->
+	  TacInductionDestruct(false,false,[ic])
+      | IDENT "edestruct";  ic = induction_clause ->
+	  TacInductionDestruct(false,true,[ic])
       | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
       | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
@@ -565,8 +587,8 @@ GEXTEND Gram
       | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
       | IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l)
       | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
-      | IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta -> 
-	  TacMove (true,id1,id2)
+      | IDENT "move"; dep = [IDENT "dependent" -> true | -> false]; 
+	  hfrom = id_or_meta; hto = move_location -> TacMove (dep,hfrom,hto)
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
       | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
 
@@ -601,16 +623,19 @@ GEXTEND Gram
 	  | IDENT "inversion" -> FullInversion
 	  | IDENT "inversion_clear" -> FullInversionClear ];
 	  hyp = quantified_hypothesis; 
-	  ids = with_names; co = OPT ["with"; c = constr -> c] ->
+	  ids = with_inversion_names; co = OPT ["with"; c = constr -> c] ->
 	    TacInversion (DepInversion (k,co,ids),hyp)
       | IDENT "simple"; IDENT "inversion";
-	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	  hyp = quantified_hypothesis; ids = with_inversion_names;
+	  cl = simple_clause ->
 	    TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
       | IDENT "inversion"; 
-	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	  hyp = quantified_hypothesis; ids = with_inversion_names;
+	  cl = simple_clause ->
 	    TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
       | IDENT "inversion_clear"; 
-	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	  hyp = quantified_hypothesis; ids = with_inversion_names; 
+	  cl = simple_clause ->
 	    TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
       | IDENT "inversion"; hyp = quantified_hypothesis; 
 	  "using"; c = constr; cl = simple_clause ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 19b7dd17e9..824ca640e8 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -188,7 +188,7 @@ module Tactic :
     val int_or_var : int or_var Gram.Entry.e
     val red_expr : raw_red_expr Gram.Entry.e
     val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
-    val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
+    val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e
     val tactic_arg : raw_tactic_arg Gram.Entry.e
     val tactic_expr : raw_tactic_expr Gram.Entry.e
     val binder_tactic : raw_tactic_expr Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index ca8b97588b..4f266f5cad 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -96,12 +96,6 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let pr_located pr (loc,x) =
-  if Flags.do_translate() && loc<>dummy_loc then
-    let (b,e) = unloc loc in
-    comment b ++ pr x ++ comment e
-  else pr x
-
 let pr_com_at n =
   if Flags.do_translate() && n <> 0 then comment n 
   else mt()
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 83339ee2f2..b9bf933ebd 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -35,7 +35,6 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool
  
 val pr_tight_coma : unit -> std_ppcmds
 
-val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
 val pr_metaid : identifier -> std_ppcmds
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2a0e755ffb..8d1dbf8756 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -142,41 +142,40 @@ let out_bindings = function
 
 let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) =
   match Genarg.genarg_tag x with
-  | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
-  | IntArgType -> pr_arg int (out_gen rawwit_int x)
-  | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x)
-  | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
-  | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
-  | IntroPatternArgType -> pr_arg pr_intro_pattern 
-      (out_gen rawwit_intro_pattern x)
-  | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
-  | VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x)
-  | RefArgType -> pr_arg prref (out_gen rawwit_ref x)
-  | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x)
-  | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
+  | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
+  | IntArgType -> int (out_gen rawwit_int x)
+  | IntOrVarArgType -> pr_or_var pr_int (out_gen rawwit_int_or_var x)
+  | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
+  | PreIdentArgType -> str (out_gen rawwit_pre_ident x)
+  | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
+  | IdentArgType -> pr_id (out_gen rawwit_ident x)
+  | VarArgType -> pr_located pr_id (out_gen rawwit_var x)
+  | RefArgType -> prref (out_gen rawwit_ref x)
+  | SortArgType -> pr_rawsort (out_gen rawwit_sort x)
+  | ConstrArgType -> prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval prc prlc (pr_or_by_notation prref))
+      pr_may_eval prc prlc (pr_or_by_notation prref)
         (out_gen rawwit_constr_may_eval x)
-  | QuantHypArgType ->
-      pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
+  | QuantHypArgType -> pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
-      pr_arg (pr_red_expr (prc,prlc,pr_or_by_notation prref))
+      pr_red_expr (prc,prlc,pr_or_by_notation prref)
         (out_gen rawwit_red_expr x)
-  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
+  | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
-      pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
+      pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x)
   | BindingsArgType -> 
-      pr_arg (pr_bindings_no_with prc prlc) (out_gen rawwit_bindings x)
+      pr_bindings_no_with prc prlc (out_gen rawwit_bindings x)
   | List0ArgType _ -> 
-      hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt()))
+      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref)
+	(fold_list0 (fun a l -> a::l) x []))
   | List1ArgType _ ->
-      hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt()))
+      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref)
+	(fold_list1 (fun a l -> a::l) x []))
   | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prref) (mt()) x)
   | PairArgType _ ->
       hov 0
         (fold_pair
-	  (fun a b -> pr_raw_generic prc prlc prtac prref a ++ spc () ++ 
-            pr_raw_generic prc prlc prtac prref b)
+	  (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prref) [a;b])
 	  x)
   | ExtraArgType s -> 
       try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
@@ -185,107 +184,105 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
 
 let rec pr_glob_generic prc prlc prtac x =
   match Genarg.genarg_tag x with
-  | BoolArgType -> pr_arg str (if out_gen globwit_bool x then "true" else "false")
-  | IntArgType -> pr_arg int (out_gen globwit_int x)
-  | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen globwit_int_or_var x)
-  | StringArgType -> spc () ++ str "\"" ++ str (out_gen globwit_string x) ++ str "\""
-  | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x)
-  | IntroPatternArgType ->
-      pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x)
-  | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x)
-  | VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x)
-  | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
-  | SortArgType -> pr_arg pr_rawsort (out_gen globwit_sort x)
-  | ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
+  | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false")
+  | IntArgType -> int (out_gen globwit_int x)
+  | IntOrVarArgType -> pr_or_var pr_int (out_gen globwit_int_or_var x)
+  | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
+  | PreIdentArgType -> str (out_gen globwit_pre_ident x)
+  | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
+  | IdentArgType -> pr_id (out_gen globwit_ident x)
+  | VarArgType -> pr_located pr_id (out_gen globwit_var x)
+  | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
+  | SortArgType -> pr_rawsort (out_gen globwit_sort x)
+  | ConstrArgType -> prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval prc prlc
-        (pr_or_var (pr_and_short_name pr_evaluable_reference)))
+      pr_may_eval prc prlc
+        (pr_or_var (pr_and_short_name pr_evaluable_reference))
         (out_gen globwit_constr_may_eval x)
   | QuantHypArgType ->
-      pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
+      pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
   | RedExprArgType ->
-      pr_arg (pr_red_expr 
-        (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)))
+      pr_red_expr 
+        (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference))
         (out_gen globwit_red_expr x)
-  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
+  | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
-      pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
+      pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x)
   | BindingsArgType -> 
-      pr_arg (pr_bindings_no_with prc prlc) (out_gen globwit_bindings x)
+      pr_bindings_no_with prc prlc (out_gen globwit_bindings x)
   | List0ArgType _ -> 
-      hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt()))
+      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac)
+	(fold_list0 (fun a l -> a::l) x []))
   | List1ArgType _ ->
-      hov 0 (fold_list1 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt()))
+      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac)
+	(fold_list1 (fun a l -> a::l) x []))
   | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prlc prtac) (mt()) x)
   | PairArgType _ ->
       hov 0
         (fold_pair
-	  (fun a b -> pr_glob_generic prc prlc prtac a ++ spc () ++ 
-            pr_glob_generic prc prlc prtac b)
+	  (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac) [a;b])
 	  x)
   | ExtraArgType s -> 
       try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> str " [no printer for " ++ str s ++ str "] "
+      with Not_found -> str "[no printer for " ++ str s ++ str "] "
 
 open Closure
 
 let rec pr_generic prc prlc prtac x =
   match Genarg.genarg_tag x with
-  | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false")
-  | IntArgType -> pr_arg int (out_gen wit_int x)
-  | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x)
-  | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\""
-  | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x)
-  | IntroPatternArgType -> 
-      pr_arg pr_intro_pattern (out_gen wit_intro_pattern x)
-  | IdentArgType -> pr_arg pr_id (out_gen wit_ident x)
-  | VarArgType -> pr_arg pr_id (out_gen wit_var x)
-  | RefArgType -> pr_arg pr_global (out_gen wit_ref x)
-  | SortArgType -> pr_arg pr_sort (out_gen wit_sort x)
-  | ConstrArgType -> pr_arg prc (out_gen wit_constr x)
-  | ConstrMayEvalArgType ->
-      pr_arg prc (out_gen wit_constr_may_eval x)
-  | QuantHypArgType ->
-      pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
+  | BoolArgType -> str (if out_gen wit_bool x then "true" else "false")
+  | IntArgType -> int (out_gen wit_int x)
+  | IntOrVarArgType -> pr_or_var pr_int (out_gen wit_int_or_var x)
+  | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
+  | PreIdentArgType -> str (out_gen wit_pre_ident x)
+  | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
+  | IdentArgType -> pr_id (out_gen wit_ident x)
+  | VarArgType -> pr_id (out_gen wit_var x)
+  | RefArgType -> pr_global (out_gen wit_ref x)
+  | SortArgType -> pr_sort (out_gen wit_sort x)
+  | ConstrArgType -> prc (out_gen wit_constr x)
+  | ConstrMayEvalArgType -> prc (out_gen wit_constr_may_eval x)
+  | QuantHypArgType -> pr_quantified_hypothesis (out_gen wit_quant_hyp x)
   | RedExprArgType ->
-      pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) 
-        (out_gen wit_red_expr x)
-  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x))
+      pr_red_expr (prc,prlc,pr_evaluable_reference) (out_gen wit_red_expr x)
+  | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x))
   | ConstrWithBindingsArgType ->
       let (c,b) = out_gen wit_constr_with_bindings x in
-      pr_arg (pr_with_bindings prc prlc) (c,out_bindings b)
+      pr_with_bindings prc prlc (c,out_bindings b)
   | BindingsArgType -> 
-      pr_arg (pr_bindings_no_with prc prlc)
-        (out_bindings (out_gen wit_bindings x))
-  | List0ArgType _ -> 
-      hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt()))
+      pr_bindings_no_with prc prlc (out_bindings (out_gen wit_bindings x))
+  | List0ArgType _ ->
+      hov 0 (pr_sequence (pr_generic prc prlc prtac)
+	(fold_list0 (fun a l -> a::l) x []))
   | List1ArgType _ ->
-      hov 0 (fold_list1 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt()))
+      hov 0 (pr_sequence (pr_generic prc prlc prtac)
+	(fold_list1 (fun a l -> a::l) x []))
   | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prlc prtac) (mt()) x)
   | PairArgType _ ->
       hov 0
-        (fold_pair
-	  (fun a b -> pr_generic prc prlc prtac a ++ spc () ++ 
-            pr_generic prc prlc prtac b)
+        (fold_pair (fun a b -> pr_sequence (pr_generic prc prlc prtac) [a;b])
 	  x)
   | ExtraArgType s -> 
       try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> str " [no printer for " ++ str s ++ str "]"
+      with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
-let rec pr_tacarg_using_rule pr_gen = function
-  | Some s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
-  | None :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule  pr_gen (l,al)
-  | [], [] -> mt ()
+let rec tacarg_using_rule_token pr_gen = function
+  | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
+  | None :: l, a :: al -> pr_gen a :: tacarg_using_rule_token pr_gen (l,al)
+  | [], [] -> []
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let pr_extend_gen prgen lev s l =
+let pr_tacarg_using_rule pr_gen l=
+  pr_sequence (fun x -> x) (tacarg_using_rule_token pr_gen l)
+
+let pr_extend_gen pr_gen lev s l =
   try 
     let tags = List.map genarg_tag l in
     let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
-    let p = pr_tacarg_using_rule prgen (pl,l) in
+    let p = pr_tacarg_using_rule pr_gen (pl,l) in
     if lev' > lev then surround p else p
   with Not_found ->
-    str s ++ prlist prgen l ++ str " (* Generic printer *)"
+    str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
 let pr_raw_extend prc prlc prtac = 
   pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference)
@@ -366,9 +363,22 @@ let pr_with_constr prc = function
   | None -> mt ()
   | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
 
+let pr_with_induction_names = function
+  | None, None -> mt ()
+  | eqpat, ipat ->
+      spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++ 
+                       pr_opt pr_intro_pattern ipat)
+
+let pr_as_intro_pattern ipat =
+  spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+
+let pr_with_inversion_names = function
+  | None -> mt ()
+  | Some ipat -> pr_as_intro_pattern ipat
+
 let pr_with_names = function
-  | IntroAnonymous -> mt ()
-  | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+  | _,IntroAnonymous -> mt ()
+  | ipat -> pr_as_intro_pattern ipat
 
 let pr_as_name = function
   | Anonymous -> mt ()
@@ -454,7 +464,7 @@ let pr_induction_kind = function
   | FullInversion -> str "inversion"
   | FullInversionClear -> str "inversion_clear"
 
-let pr_lazy lz = if lz then str "lazy " else mt ()
+let pr_lazy lz = if lz then str "lazy" else mt ()
 
 let pr_match_pattern pr_pat = function
   | Term a -> pr_pat a
@@ -493,8 +503,9 @@ let pr_funvar = function
   | None -> spc () ++ str "_"
   | Some id -> spc () ++ pr_id id
 
-let pr_let_clause k pr (id,t) =
-  hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++ pr (TacArg t))
+let pr_let_clause k pr (id,(bl,t)) =
+  hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++ 
+         str " :=" ++ brk (1,1) ++ pr (TacArg t))
 
 let pr_let_clauses recflag pr = function
   | hd::tl ->
@@ -603,6 +614,10 @@ let pr_intarg n = spc () ++ int n in
 (* Some printing combinators *)
 let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
 
+let extract_binders = function
+  | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+  | body -> ([],body) in
+
 let pr_binder_fix (nal,t) =
 (*  match t with
   | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
@@ -648,7 +663,7 @@ let pr_cofix_tac (id,c) =
   (* Printing tactics as arguments *)
 let rec pr_atom0 = function
   | TacIntroPattern [] -> str "intros"
-  | TacIntroMove (None,None) -> str "intro"
+  | TacIntroMove (None,hto) when hto = no_move -> str "intro"
   | TacAssumption -> str "assumption"
   | TacAnyConstructor (false,None) -> str "constructor"
   | TacAnyConstructor (true,None) -> str "econstructor"
@@ -676,12 +691,10 @@ and pr_atom1 = function
       hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
   | TacIntrosUntil h ->
       hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
-  | TacIntroMove (None,None) as t -> pr_atom0 t
-  | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1
-  | TacIntroMove (ido1,Some id2) ->
-      hov 1
-      (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
-       pr_lident id2)
+  | TacIntroMove (None,hto) as t when hto = no_move -> pr_atom0 t
+  | TacIntroMove (Some id,hto) when hto = no_move -> str "intro " ++ pr_id id
+  | TacIntroMove (ido,hto) ->
+      hov 1 (str"intro" ++ pr_opt pr_id ido ++ pr_move_location pr_ident hto)
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
@@ -689,7 +702,7 @@ and pr_atom1 = function
   | TacApply (a,ev,cb) ->
       hov 1 ((if a then mt() else str "simple ") ++
              str (with_evars ev "apply") ++ spc () ++ 
-             pr_with_bindings cb)
+             prlist_with_sep pr_coma pr_with_bindings cb)
   | TacElim (ev,cb,cbo) ->
       hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ 
         pr_opt pr_eliminator cbo)
@@ -741,22 +754,17 @@ and pr_atom1 = function
 	     ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
 *)
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
-      hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (ev,h,e,ids,cl) ->
-      hov 1 (str (with_evars ev "induction") ++ spc () ++
-	     prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
-	     pr_with_names ids ++
-             pr_opt pr_eliminator e ++
-             pr_opt_no_spc (pr_clauses pr_ident) cl)
-  | TacSimpleDestruct h ->
-      hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (ev,h,e,ids,cl) ->
-      hov 1 (str (with_evars ev "destruct") ++ spc () ++
-             prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ 
-	     pr_with_names ids ++
-             pr_opt pr_eliminator e ++
-             pr_opt_no_spc (pr_clauses pr_ident) cl)
+  | TacSimpleInductionDestruct (isrec,h) ->
+      hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
+             ++ pr_arg pr_quantified_hypothesis h)
+  | TacInductionDestruct (isrec,ev,l) ->
+      hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
+             spc () ++
+             prlist_with_sep pr_coma (fun (h,e,ids,cl) ->
+	       prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
+	       pr_with_induction_names ids ++
+               pr_opt pr_eliminator e ++
+               pr_opt_no_spc (pr_clauses pr_ident) cl) l)
   | TacDoubleInduction (h1,h2) ->
       hov 1
         (str "double induction" ++  
@@ -800,8 +808,8 @@ and pr_atom1 = function
       (* Rem: only b = true is available for users *)
       assert b;
       hov 1
-        (str "move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
-	 str "after" ++ brk (1,1) ++ pr_ident id2)
+        (str "move" ++ brk (1,1) ++ pr_ident id1 ++ 
+	 pr_move_location pr_ident id2)
   | TacRename l ->
       hov 1
         (str "rename" ++ brk (1,1) ++
@@ -856,11 +864,11 @@ and pr_atom1 = function
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
-      pr_with_names ids ++ pr_with_constr pr_constr c)
+      pr_with_inversion_names ids ++ pr_with_constr pr_constr c)
   | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
       hov 1 (pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
-      pr_with_names ids ++ pr_simple_clause pr_ident cl)
+      pr_with_inversion_names ids ++ pr_simple_clause pr_ident cl)
   | TacInversion (InversionUsing (c,cl),hyp) ->
       hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ 
       spc () ++ str "using" ++ spc () ++ pr_constr c ++ 
@@ -878,6 +886,7 @@ let rec pr_tac inherited tac =
         str "using " ++ pr_id s),
       labstract
   | TacLetIn (recflag,llc,u) ->
+      let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
       v 0
        (hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++
        fnl () ++ pr_tac (llet,E) u),
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 31a626ceac..b672e9c23e 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -78,6 +78,8 @@ val pr_extend :
   (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
     string -> typed_generic_argument list -> std_ppcmds
 
+val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
 val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds
 
 val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 1060928d12..99d8e3c4a1 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -804,10 +804,7 @@ let rec pr_vernac = function
 	  (Global.env())
 	  body in
       hov 1
-        (((*if !Flags.p1 then
-	  (if rc then str "Recursive " else mt()) ++
-	  str "Tactic Definition " else*)
-	    (* Rec by default *) str "Ltac ") ++
+        ((str "Ltac ") ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_pattern_expr
diff --git a/parsing/printer.ml b/parsing/printer.ml
index f59f9f2f3e..561c85785d 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -28,6 +28,7 @@ open Refiner
 open Pfedit
 open Ppconstr
 open Constrextern
+open Tacexpr
 
 let emacs_str s alts = 
   match !Flags.print_emacs, !Flags.print_emacs_safechar with
@@ -421,14 +422,14 @@ let pr_prim_rule = function
   | Intro id -> 
       str"intro " ++ pr_id id
 	
-  | Intro_replacing id -> 
-      (str"intro replacing "  ++ pr_id id)
-	
-  | Cut (b,id,t) ->
-      if b then
-        (str"assert " ++ pr_constr t)
-      else
-        (str"cut " ++ pr_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
+  | Cut (b,replace,id,t) ->
+     if b then
+       (* TODO: express "replace" *)
+       (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
+     else
+       let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
+       (str"cut " ++ pr_constr t ++ 
+        str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 	
   | FixRule (f,n,[]) ->
       (str"fix " ++ pr_id f ++ str"/" ++ int n)
@@ -472,7 +473,7 @@ let pr_prim_rule = function
       
   | Move (withdep,id1,id2) ->
       (str (if withdep then "dependent " else "") ++
-	 str"move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+	 str"move "  ++ pr_id id1 ++ pr_move_location pr_id id2)
 
   | Rename (id1,id2) ->
       (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index a4e0cd570f..32f0519480 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -22,6 +22,7 @@ open Termops
 open Evd
 open Proof_type
 open Rawterm
+open Tacexpr
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 66a74ad162..56afbc9bee 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -71,7 +71,7 @@ let mlexpr_of_by_notation f = function
   | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >>
 
 let mlexpr_of_intro_pattern = function
-  | Genarg.IntroWildcard loc -> <:expr< Genarg.IntroWildcard $mlexpr_of_loc loc$ >>
+  | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
   | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
   | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
   | Genarg.IntroIdentifier id ->
@@ -242,6 +242,11 @@ let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
 let mlexpr_of_constr_with_binding =
   mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
 
+let mlexpr_of_move_location f = function
+  | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >>
+  | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >>
+  | Tacexpr.MoveToEnd b -> <:expr< Tacexpr.MoveToEnd $mlexpr_of_bool b$ >>
+
 let mlexpr_of_induction_arg = function
   | Tacexpr.ElimOnConstr c ->
       <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >>
@@ -282,13 +287,13 @@ let mlexpr_of_message_token = function
 let rec mlexpr_of_atomic_tactic = function
   (* Basic tactics *)
   | Tacexpr.TacIntroPattern pl ->
-      let pl = mlexpr_of_list mlexpr_of_intro_pattern pl in
+      let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in
       <:expr< Tacexpr.TacIntroPattern $pl$ >>
   | Tacexpr.TacIntrosUntil h ->
       <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacIntroMove (idopt,idopt') ->
       let idopt = mlexpr_of_ident_option idopt in
-      let idopt'=mlexpr_of_option (mlexpr_of_located mlexpr_of_ident) idopt' in
+      let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in
       <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >>
   | Tacexpr.TacAssumption ->
       <:expr< Tacexpr.TacAssumption >>
@@ -299,7 +304,7 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacVmCastNoCheck c ->
       <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacApply (b,false,cb) ->
-      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_constr_with_binding cb$ >>
+      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >>
   | Tacexpr.TacElim (false,cb,cbo) ->
       let cb = mlexpr_of_constr_with_binding cb in
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
@@ -335,7 +340,7 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
   | Tacexpr.TacAssert (t,ipat,c) ->
-      let ipat = mlexpr_of_intro_pattern ipat in
+      let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in
       <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ 
 	      $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
@@ -351,18 +356,18 @@ let rec mlexpr_of_atomic_tactic = function
 	      $mlexpr_of_bool b$ >>
 
   (* Derived basic tactics *)
-  | Tacexpr.TacSimpleInduction h ->
-      <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >>
-  | Tacexpr.TacNewInduction (false,cl,cbo,ids,cls) ->
-      let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_intro_pattern ids in
-      <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >>
-  | Tacexpr.TacSimpleDestruct h ->
-      <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacNewDestruct (false,c,cbo,ids,cls) ->
-      let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_intro_pattern ids in
-      <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >>
+  | Tacexpr.TacSimpleInductionDestruct (isrec,h) ->
+      <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$
+                  $mlexpr_of_quantified_hypothesis h$ >>
+  | Tacexpr.TacInductionDestruct (isrec,ev,l) ->
+      <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ 
+	$mlexpr_of_list (mlexpr_of_quadruple 
+	  (mlexpr_of_list mlexpr_of_induction_arg)
+	  (mlexpr_of_option mlexpr_of_constr_with_binding)
+	  (mlexpr_of_pair
+	    (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
+	    (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))
+	  (mlexpr_of_option mlexpr_of_clause)) l$ >>
 
   (* Context management *)
   | Tacexpr.TacClear (b,l) ->
@@ -374,7 +379,7 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacMove (dep,id1,id2) ->
       <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$
               $mlexpr_of_hyp id1$
-              $mlexpr_of_hyp id2$ >>
+              $mlexpr_of_move_location mlexpr_of_hyp id2$ >>
 
   (* Constructors *)
   | Tacexpr.TacLeft (ev,l) ->
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 513d345b56..9b59ba8e5b 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -53,6 +53,11 @@ let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
   let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
   <:expr< ($e1$, $e2$, $e3$) >>
 
+let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)=
+  let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in
+  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in
+  <:expr< ($e1$, $e2$, $e3$, $e4$) >>
+
 (* We don't give location for tactic quotation! *)
 let loc = dummy_loc
 
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index f6660c9d56..a160310e44 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -20,6 +20,10 @@ val mlexpr_of_triple :
   ('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr)
     -> 'a * 'b * 'c -> MLast.expr
 
+val mlexpr_of_quadruple :
+  ('a -> MLast.expr) -> ('b -> MLast.expr) ->
+    ('c -> MLast.expr) -> ('d -> MLast.expr) -> 'a * 'b * 'c * 'd -> MLast.expr
+
 val mlexpr_of_bool : bool -> MLast.expr
 
 val mlexpr_of_int : int -> MLast.expr