Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

26 files changed, 747 insertions, 838 deletions

diff --git a/printing/genprint.ml b/printing/genprint.ml
index ade69ef831..0ec35e07be 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,8 +19,9 @@ module PrintObj =
 struct
   type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
   let name = "printer"
-  let default wit = match unquote (rawwit wit) with
-  | ExtraArgType name ->
+  let default wit = match wit with
+  | ExtraArg tag ->
+    let name = ArgT.repr tag in
     let printer = {
       raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
       glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
@@ -40,6 +41,6 @@ let raw_print wit v = (Print.obj wit).raw v
 let glb_print wit v = (Print.obj wit).glb v
 let top_print wit v = (Print.obj wit).top v
 
-let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v
-let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v
-let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v
+let generic_raw_print (GenArg (Rawwit w, v)) = raw_print w v
+let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v
+let generic_top_print (GenArg (Topwit w, v)) = top_print w v
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 5b91d6d216..6e6626f2f6 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index d09af6d2ac..5e86c6bd76 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -33,9 +33,9 @@ and pr_intro_pattern_action prc = function
   | IntroRewrite false -> str "<-"
 
 and pr_or_and_intro_pattern prc = function
-  | [pl] ->
+  | IntroAndPattern pl ->
       str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
-  | pll ->
+  | IntroOrPattern pll ->
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
       ++ str "]"
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index 1d915ef8c5..fe8c779ff4 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 4f26b82424..511f93569c 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,7 +20,6 @@ type t =
   | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
   | ARawTacticExpr        of raw_tactic_expr
   | ARawAtomicTacticExpr  of raw_atomic_tactic_expr
-  | ATacticExpr           of tactic_expr
   | AAtomicTacticExpr     of atomic_tactic_expr
 
 let tag_of_annotation = function
@@ -32,7 +31,6 @@ let tag_of_annotation = function
   | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr"
   | ARawTacticExpr _        -> "raw_tactic_expr"
   | ARawAtomicTacticExpr _  -> "raw_atomic_tactic_expr"
-  | ATacticExpr _           -> "tactic_expr"
   | AAtomicTacticExpr _     -> "atomic_tactic_expr"
 
 let attributes_of_annotation a =
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index bc345c347b..a0fef1a757 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,7 +23,6 @@ type t =
   | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
   | ARawTacticExpr        of raw_tactic_expr
   | ARawAtomicTacticExpr  of raw_atomic_tactic_expr
-  | ATacticExpr           of tactic_expr
   | AAtomicTacticExpr     of atomic_tactic_expr
 
 val tag_of_annotation : t -> string
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 650b8f7262..1866ca5042 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -136,12 +136,10 @@ end) = struct
 
   let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
-  let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
-
   let pr_univ l =
     match l with
-      | [x] -> str x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+      | [_,x] -> str x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -153,11 +151,11 @@ end) = struct
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
-    let id = tag_ref (str (Id.to_string id)) in
+    let id = tag_ref (pr_id id) in
     let sl = match List.rev (DirPath.repr sl) with
     | [] -> mt ()
     | sl ->
-      let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in
+      let pr dir = tag_path (pr_id dir) ++ str "." in
       prlist pr sl
     in
     sl ++ id
@@ -174,7 +172,7 @@ end) = struct
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some u -> str u
+        | Some (_,u) -> str u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
@@ -182,7 +180,7 @@ end) = struct
 
   let pr_reference = function
   | Qualid (_, qid) -> pr_qualid qid
-  | Ident (_, id) -> tag_var (str (Id.to_string id))
+  | Ident (_, id) -> tag_var (pr_id id)
 
   let pr_cref ref us =
     pr_reference ref ++ pr_universe_instance us
@@ -246,16 +244,16 @@ end) = struct
       | CPatAlias (_, p, id) ->
         pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
 
-      | CPatCstr (_,c, [], []) ->
+      | CPatCstr (_,c, None, []) ->
         pr_reference c, latom
 
-      | CPatCstr (_, c, [], args) ->
+      | CPatCstr (_, c, None, args) ->
         pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
 
-      | CPatCstr (_, c, args, []) ->
+      | CPatCstr (_, c, Some args, []) ->
         str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
 
-      | CPatCstr (_, c, expl_args, extra_args) ->
+      | CPatCstr (_, c, Some expl_args, extra_args) ->
         surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
         ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
 
@@ -457,7 +455,7 @@ end) = struct
         (pr_decl true) dl ++
         fnl() ++ keyword "for" ++ spc () ++ pr_id id
 
-  let pr_asin pr (na,indnalopt) =
+  let pr_asin pr na indnalopt =
     (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
       | Some na -> spc () ++ keyword "as" ++ spc () ++  pr_lname na
       | None -> mt ()) ++
@@ -465,8 +463,8 @@ end) = struct
         | None -> mt ()
         | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
 
-  let pr_case_item pr (tm,asin) =
-    hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
+  let pr_case_item pr (tm,as_clause, in_clause) =
+    hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause)
 
   let pr_case_type pr po =
     match po with
@@ -595,28 +593,20 @@ end) = struct
           return (p, lproj)
       | CApp (_,(None,a),l) ->
         return (pr_app (pr mt) a l, lapp)
-      | CRecord (_,w,l) ->
-        let beg =
-          match w with
-            | None ->
-              spc ()
-            | Some t ->
-              spc () ++ pr spc ltop t ++ spc ()
-              ++ keyword "with" ++ spc ()
-        in
+      | CRecord (_,l) ->
         return (
-          hv 0 (str"{|" ++ beg ++
+          hv 0 (str"{|" ++ spc () ++
                   prlist_with_sep pr_semicolon
                   (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
                 ++ str" |}"),
           latom
         )
-      | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+      | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
               hov 0 (pr_patt ltop p ++
-                       pr_asin (pr_dangling_with_for mt pr) asin ++
+                       pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++
                        str " :=" ++ pr spc ltop c ++
                        pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
                        spc () ++ keyword "in" ++ pr spc ltop b)),
@@ -638,13 +628,13 @@ end) = struct
       | CLetTuple (_,nal,(na,po),c,b) ->
         return (
           hv 0 (
-            keyword "let" ++ spc () ++
-              hov 0 (str "(" ++
+            hov 2 (keyword "let" ++ spc () ++
+              hov 1 (str "(" ++
                        prlist_with_sep sep_v pr_lname nal ++
                        str ")" ++
-                       pr_simple_return_type (pr mt) na po ++ str " :=" ++
-                       pr spc ltop c ++ spc ()
-                     ++ keyword "in") ++
+                       pr_simple_return_type (pr mt) na po ++ str " :=") ++
+                       pr spc ltop c
+                     ++ keyword " in") ++
               pr spc ltop b),
           lletin
         )
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 6e8d3b04c4..0241633c61 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index b7eb9b1fff..c711dd8f7f 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e8ccd29c8a..19536d9f83 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -26,11 +26,11 @@ open Printer
 
 let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
-type grammar_terminals = string option list
+type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
-  pptac_args : argument_type list;
-  pptac_prods : int * grammar_terminals;
+  pptac_level : int;
+  pptac_prods : grammar_terminals;
 }
 
 (* ML Extensions *)
@@ -61,14 +61,14 @@ type 'a glob_extra_genarg_printer =
 type 'a extra_genarg_printer =
     (Term.constr -> std_ppcmds) ->
     (Term.constr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
 let genarg_pprule = ref String.Map.empty
 
 let declare_extra_genarg_pprule wit f g h =
-  let s = match unquote (topwit wit) with
-    | ExtraArgType s -> s
+  let s = match wit with
+    | ExtraArg s -> ArgT.repr s
     | _ -> error
       "Can declare a pretty-printing rule only for extra argument types."
   in
@@ -94,8 +94,6 @@ module Make
         : raw_tactic_expr -> std_ppcmds -> std_ppcmds
       val tag_raw_atomic_tactic_expr
         : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_tactic_expr
-        : tactic_expr -> std_ppcmds -> std_ppcmds
       val tag_atomic_tactic_expr
         : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
   end)
@@ -106,6 +104,24 @@ module Make
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
+  let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with
+  | Val.List tag ->
+    pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x
+  | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x
+  | Val.Pair (tag1, tag2) ->
+    str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++
+      pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")"
+  | Val.Base t ->
+    let name = Val.repr t in
+    let default = str "<" ++ str name ++ str ">" in
+    match ArgT.name name with
+    | None -> default
+    | Some (ArgT.Any arg) ->
+      let wit = ExtraArg arg in
+      match Val.eq (val_tag (Topwit wit)) (Val.Base t) with
+      | None -> default
+      | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+
   let pr_with_occurrences pr (occs,c) =
     match occs with
       | AllOccurrences ->
@@ -264,150 +280,89 @@ module Make
 
   let with_evars ev s = if ev then "e" ^ s else s
 
+  let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
 
-  let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
-    match Genarg.genarg_tag x with
-      | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
-      | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
-      | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
-      | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
-      | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
-      | ConstrMayEvalArgType ->
-        pr_may_eval prc prlc (pr_or_by_notation prref) prpat
-          (out_gen (rawwit wit_constr_may_eval) x)
-      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
-      | RedExprArgType ->
-        pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
-          (out_gen (rawwit wit_red_expr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
-      | ConstrWithBindingsArgType ->
-        pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
-      | BindingsArgType ->
-        pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
-          pr_sequence map (raw l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match raw o with
+  let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
+        let ans = pr_sequence map x in
+        hov_if_not_empty 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
-          | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
+          | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
         in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = raw o in
-          let p = in_gen (rawwit wit1) p in
-          let q = in_gen (rawwit wit2) q in
-          pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
-        in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_raw_print x
-
-
-  let rec pr_glb_generic prc prlc prtac prpat x =
-    match Genarg.genarg_tag x with
-      | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
-      | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
-      | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
-      | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
-      | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
-      | ConstrMayEvalArgType ->
-        pr_may_eval prc prlc
-          (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
-          (out_gen (glbwit wit_constr_may_eval) x)
-      | QuantHypArgType ->
-        pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
-      | RedExprArgType ->
-        pr_red_expr
-          (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
-          (out_gen (glbwit wit_red_expr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
-      | ConstrWithBindingsArgType ->
-        pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
-      | BindingsArgType ->
-        pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
-          pr_sequence map (glb l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match glb o with
+        hov_if_not_empty 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (rawwit wit1) p in
+        let q = in_gen (rawwit wit2) q in
+        hov_if_not_empty 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q])
+      | ExtraArg s ->
+        try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
+        with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
+
+
+  let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
+        let ans = pr_sequence map x in
+        hov_if_not_empty 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
-          | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
-        in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = glb o in
-          let p = in_gen (glbwit wit1) p in
-          let q = in_gen (glbwit wit2) q in
-          pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
+          | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
         in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_glb_print x
-
-  let rec pr_top_generic prc prlc prtac prpat x =
-    match Genarg.genarg_tag x with
-      | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
-      | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
-      | VarArgType -> pr_id (out_gen (topwit wit_var) x)
-      | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
-      | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
-      | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
-      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
-      | RedExprArgType ->
-        pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
-          (out_gen (topwit wit_red_expr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
-      | ConstrWithBindingsArgType ->
-        let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
-        pr_with_bindings prc prlc (c,b)
-      | BindingsArgType ->
-        pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
-          pr_sequence map (top l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match top o with
+        hov_if_not_empty 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (glbwit wit1) p in
+        let q = in_gen (glbwit wit2) q in
+        let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in
+        hov_if_not_empty 0 ans
+      | ExtraArg s ->
+        try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x)
+        with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x)
+
+  let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
+        let ans = pr_sequence map x in
+        hov_if_not_empty 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
-          | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
-        in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = top o in
-          let p = in_gen (topwit wit1) p in
-          let q = in_gen (topwit wit2) q in
-          pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
+          | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x)
         in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_top_print x
+        hov_if_not_empty 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (topwit wit1) p in
+        let q = in_gen (topwit wit2) q in
+        let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in
+        hov_if_not_empty 0 ans
+      | ExtraArg s ->
+        try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x)
+        with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x)
 
   let rec tacarg_using_rule_token pr_gen = function
-    | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
-    | None :: l, a :: al ->
+    | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
+    | Egramml.GramNonTerminal _ :: l, a :: al ->
       let r = tacarg_using_rule_token pr_gen (l,al) in
       pr_gen a :: r
     | [], [] -> []
     | _ -> failwith "Inconsistent arguments of extended tactic"
 
+  let filter_arg = function
+  | Egramml.GramTerminal _ -> None
+  | Egramml.GramNonTerminal (_, Rawwit t, _) -> Some (ArgumentType t)
+
   let pr_tacarg_using_rule pr_gen l =
     let l = match l with
-    | (Some s :: l, al) ->
+    | (Egramml.GramTerminal s :: l, al) ->
       (** First terminal token should be considered as the name of the tactic,
           so we tag it differently than the other terminal tokens. *)
       primitive s :: (tacarg_using_rule_token pr_gen (l, al))
@@ -415,13 +370,14 @@ module Make
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+  let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
     try
       let pp_rules = Hashtbl.find prtac_tab s in
       let pp = pp_rules.(i) in
-      let (lev', pl) = pp.pptac_prods in
-      let p = pr_tacarg_using_rule pr_gen (pl,l) in
-      if lev' > lev then surround p else p
+      let args = List.map_filter filter_arg pp.pptac_prods in
+      let () = if not (List.for_all2eq check args l) then raise Not_found in
+      let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
+      if pp.pptac_level > lev then surround p else p
     with Not_found ->
       let name =
         str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
@@ -433,28 +389,31 @@ module Make
       in
       str "<" ++ name ++ str ">" ++ args
 
-  let pr_alias_gen pr_gen lev key l =
+  let pr_alias_gen check pr_gen lev key l =
     try
       let pp = KNmap.find key !prnotation_tab in
-      let (lev', pl) = pp.pptac_prods in
-      let p = pr_tacarg_using_rule pr_gen (pl, l) in
-      if lev' > lev then surround p else p
+      let args = List.map_filter filter_arg pp.pptac_prods in
+      let () = if not (List.for_all2eq check args l) then raise Not_found in
+      let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
+      if pp.pptac_level > lev then surround p else p
     with Not_found ->
       KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
-  let pr_raw_extend prc prlc prtac prpat =
-    pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
-  let pr_glob_extend prc prlc prtac prpat =
-    pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
-  let pr_extend prc prlc prtac prpat =
-    pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+  let check_type t arg = match arg with
+  | TacGeneric arg -> argument_type_eq t (genarg_tag arg)
+  | _ -> argument_type_eq t (ArgumentType wit_tactic)
+
+  let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
+
+  let pr_raw_extend_rec prc prlc prtac prpat =
+    pr_extend_gen check_type (pr_farg prtac)
+  let pr_glob_extend_rec prc prlc prtac prpat =
+    pr_extend_gen check_type (pr_farg prtac)
 
   let pr_raw_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+    pr_alias_gen check_type (pr_farg prtac)
   let pr_glob_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
-  let pr_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_top_generic prc prlc prtac prpat)
+    pr_alias_gen check_type (pr_farg prtac)
 
   (**********************************************************************)
   (* The tactic printer                                                 *)
@@ -563,9 +522,8 @@ module Make
     | ipat ->
       spc() ++ prc c ++ pr_as_ipat prdc ipat
 
-  let pr_by_tactic prt = function
-    | TacId [] -> mt ()
-    | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac
+  let pr_by_tactic prt tac =
+    spc() ++ keyword "by" ++ spc () ++ prt tac
 
   let pr_hyp_location pr_id = function
     | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
@@ -578,7 +536,7 @@ module Make
         str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
       ) occs
 
-  let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp)
+  let pr_in pp = hov 0 (keyword "in" ++ pp)
 
   let pr_simple_hyp_clause pr_id = function
     | [] -> mt ()
@@ -586,8 +544,7 @@ module Make
 
   let pr_in_hyp_as prc pr_id = function
     | None -> mt ()
-    | Some (clear,id,ipat) ->
-      pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat
+    | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
 
   let pr_clauses default_is_concl pr_id = function
     | { onhyps=Some []; concl_occs=occs }
@@ -712,20 +669,13 @@ module Make
             str " ]")
 
   let pr_hintbases = function
-    | None -> spc () ++ keyword "with" ++ str" *"
+    | None -> keyword "with" ++ str" *"
     | Some [] -> mt ()
-    | Some l ->
-      spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
+    | Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
 
   let pr_auto_using prc = function
     | [] -> mt ()
-    | l -> spc () ++
-      hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
-
-  let string_of_debug = function
-    | Off -> ""
-    | Debug -> "debug "
-    | Info -> "info_"
+    | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
   let pr_then () = str ";"
 
@@ -752,7 +702,6 @@ module Make
   type 'a printer = {
     pr_tactic    : tolerability -> 'tacexpr -> std_ppcmds;
     pr_constr    : 'trm -> std_ppcmds;
-    pr_uconstr   : 'utrm -> std_ppcmds;
     pr_lconstr   : 'trm -> std_ppcmds;
     pr_dconstr   : 'dtrm -> std_ppcmds;
     pr_pattern   : 'pat -> std_ppcmds;
@@ -761,13 +710,12 @@ module Make
     pr_reference : 'ref -> std_ppcmds;
     pr_name      : 'nam -> std_ppcmds;
     pr_generic   : 'lev generic_argument -> std_ppcmds;
-    pr_extend    : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds;
-    pr_alias     : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
+    pr_extend    : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
+    pr_alias     : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
   }
 
   constraint 'a = <
       term      :'trm;
-      utrm      :'utrm;
       dterm     :'dtrm;
       pattern   :'pat;
       constant  :'cst;
@@ -777,306 +725,246 @@ module Make
       level     :'lev
     >
 
-    let make_pr_tac pr strip_prod_binders tag_atom tag =
-
-        (* some shortcuts *)
-        let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
-        let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
-        let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
-        let pr_with_bindings_arg_full = pr_with_bindings_arg in
-        let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
-        let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
-
-        let pr_constrarg c = spc () ++ pr.pr_constr c in
-        let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
-        let pr_intarg n = spc () ++ int n in
-
-        (* Some printing combinators *)
-        let pr_eliminator cb = keyword "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
-              | _ ->*)
-          let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
-          spc() ++ hov 1 (str"(" ++ s ++ str")") in
-
-        let pr_fix_tac (id,n,c) =
-          let rec set_nth_name avoid n = function
-          (nal,ty)::bll ->
-            if n <= List.length nal then
-              match List.chop (n-1) nal with
-                  _, (_,Name id) :: _ -> id, (nal,ty)::bll
-                | bef, (loc,Anonymous) :: aft ->
-                  let id = next_ident_away (Id.of_string"y") avoid in
-                  id, ((bef@(loc,Name id)::aft, ty)::bll)
-                | _ -> assert false
-            else
-              let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
-              (id,(nal,ty)::bll')
-            | [] -> assert false in
-          let (bll,ty) = strip_prod_binders n c in
-          let names =
-            List.fold_left
-              (fun ln (nal,_) -> List.fold_left
-                (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
-                ln nal)
-              [] bll in
-          let idarg,bll = set_nth_name names n bll in
-          let annot = match names with
-            | [_] ->
-              mt ()
-            | _ ->
-              spc() ++ str"{"
-              ++ keyword "struct" ++ spc ()
-              ++ pr_id idarg ++ str"}"
-          in
-          hov 1 (str"(" ++ pr_id id ++
-                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
-                   pr_lconstrarg ty ++ str")") in
-        (*  spc() ++
-            hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
-            c)
+    let pr_atom pr strip_prod_binders tag_atom =
+      let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+      let pr_with_bindings_arg_full = pr_with_bindings_arg in
+      let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
+      let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+
+      let pr_constrarg c = spc () ++ pr.pr_constr c in
+      let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+      let pr_intarg n = spc () ++ int n in
+
+      (* Some printing combinators *)
+      let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
+
+      let pr_binder_fix (nal,t) =
+        (*  match t with
+            | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+            | _ ->*)
+        let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+        spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+      let pr_fix_tac (id,n,c) =
+        let rec set_nth_name avoid n = function
+        (nal,ty)::bll ->
+          if n <= List.length nal then
+            match List.chop (n-1) nal with
+                _, (_,Name id) :: _ -> id, (nal,ty)::bll
+              | bef, (loc,Anonymous) :: aft ->
+                let id = next_ident_away (Id.of_string"y") avoid in
+                id, ((bef@(loc,Name id)::aft, ty)::bll)
+              | _ -> assert false
+          else
+            let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+            (id,(nal,ty)::bll')
+          | [] -> assert false in
+        let (bll,ty) = strip_prod_binders n c in
+        let names =
+          List.fold_left
+            (fun ln (nal,_) -> List.fold_left
+              (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+              ln nal)
+            [] bll in
+        let idarg,bll = set_nth_name names n bll in
+        let annot = match names with
+          | [_] ->
+            mt ()
+          | _ ->
+            spc() ++ str"{"
+            ++ keyword "struct" ++ spc ()
+            ++ pr_id idarg ++ str"}"
+        in
+        hov 1 (str"(" ++ pr_id id ++
+                  prlist pr_binder_fix bll ++ annot ++ str" :" ++
+                  pr_lconstrarg ty ++ str")") in
+      (*  spc() ++
+          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+          c)
+      *)
+      let pr_cofix_tac (id,c) =
+        hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+      (* Printing tactics as arguments *)
+      let rec pr_atom0 a = tag_atom a (match a with
+        | TacIntroPattern [] -> primitive "intros"
+        | TacIntroMove (None,MoveLast) -> primitive "intro"
+        | t -> str "(" ++ pr_atom1 t ++ str ")"
+      )
+
+      (* Main tactic printer *)
+      and pr_atom1 a = tag_atom a (match a with
+        (* Basic tactics *)
+        | TacIntroPattern [] as t ->
+          pr_atom0 t
+        | TacIntroPattern (_::_ as p) ->
+          hov 1 (primitive "intros" ++ spc () ++
+                    prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
+        | TacIntroMove (None,MoveLast) as t ->
+          pr_atom0 t
+        | TacIntroMove (Some id,MoveLast) ->
+          primitive "intro" ++ spc () ++ pr_id id
+        | TacIntroMove (ido,hto) ->
+          hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
+                    Miscprint.pr_move_location pr.pr_name hto)
+        | TacExact c ->
+          hov 1 (primitive "exact" ++ pr_constrarg c)
+        | TacApply (a,ev,cb,inhyp) ->
+          hov 1 (
+            (if a then mt() else primitive "simple ") ++
+              primitive (with_evars ev "apply") ++ spc () ++
+              prlist_with_sep pr_comma pr_with_bindings_arg cb ++
+              pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
+          )
+        | TacElim (ev,cb,cbo) ->
+          hov 1 (
+            primitive (with_evars ev "elim")
+            ++ pr_arg pr_with_bindings_arg cb
+            ++ pr_opt pr_eliminator cbo)
+        | TacCase (ev,cb) ->
+          hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+        | TacMutualFix (id,n,l) ->
+          hov 1 (
+            primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
+            ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
+        | TacMutualCofix (id,l) ->
+          hov 1 (
+            primitive "cofix" ++ spc () ++ pr_id id ++ spc()
+            ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
+          )
+        | TacAssert (b,Some tac,ipat,c) ->
+          hov 1 (
+            primitive (if b then "assert" else "enough") ++
+              pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+              pr_by_tactic (pr.pr_tactic ltop) tac
+          )
+        | TacAssert (_,None,ipat,c) ->
+          hov 1 (
+            primitive "pose proof"
+            ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+          )
+        | TacGeneralize l ->
+          hov 1 (
+            primitive "generalize" ++ spc ()
+            ++ prlist_with_sep pr_comma (fun (cl,na) ->
+              pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+              l
+          )
+        | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
+          hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+        | TacLetTac (na,c,cl,b,e) ->
+          hov 1 (
+            (if b then primitive "set" else primitive "remember") ++
+              (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
+                else pr_pose_as_style pr.pr_constr na c) ++
+              pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
+              pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
+        (*  | TacInstantiate (n,c,ConclLocation ()) ->
+            hov 1 (str "instantiate" ++ spc() ++
+            hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+            pr_lconstrarg c ++ str ")" ))
+            | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+            hov 1 (str "instantiate" ++ spc() ++
+            hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+            pr_lconstrarg c ++ str ")" )
+            ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
         *)
-        let pr_cofix_tac (id,c) =
-          hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
-
-        (* Printing tactics as arguments *)
-        let rec pr_atom0 a = tag_atom a (match a with
-          | TacIntroPattern [] -> primitive "intros"
-          | TacIntroMove (None,MoveLast) -> primitive "intro"
-          | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial"
-          | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto"
-          | TacClear (true,[]) -> primitive "clear"
-          | t -> str "(" ++ pr_atom1 t ++ str ")"
-        )
-
-        (* Main tactic printer *)
-        and pr_atom1 a = tag_atom a (match a with
-          (* Basic tactics *)
-          | TacIntroPattern [] as t ->
-            pr_atom0 t
-          | TacIntroPattern (_::_ as p) ->
-            hov 1 (primitive "intros" ++ spc () ++
-                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-          | TacIntroMove (None,MoveLast) as t ->
-            pr_atom0 t
-          | TacIntroMove (Some id,MoveLast) ->
-            primitive "intro" ++ spc () ++ pr_id id
-          | TacIntroMove (ido,hto) ->
-            hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
-                     Miscprint.pr_move_location pr.pr_name hto)
-          | TacExact c ->
-            hov 1 (primitive "exact" ++ pr_constrarg c)
-          | TacApply (a,ev,cb,inhyp) ->
-            hov 1 (
-              (if a then mt() else primitive "simple ") ++
-                primitive (with_evars ev "apply") ++ spc () ++
-                prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-                pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp
-            )
-          | TacElim (ev,cb,cbo) ->
-            hov 1 (
-              primitive (with_evars ev "elim")
-              ++ pr_arg pr_with_bindings_arg cb
-              ++ pr_opt pr_eliminator cbo)
-          | TacCase (ev,cb) ->
-            hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
-          | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
-          | TacMutualFix (id,n,l) ->
-            hov 1 (
-              primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
-              ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
-          | TacCofix ido ->
-            hov 1 (primitive "cofix" ++ pr_opt pr_id ido)
-          | TacMutualCofix (id,l) ->
-            hov 1 (
-              primitive "cofix" ++ spc () ++ pr_id id ++ spc()
-              ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
-            )
-          | TacAssert (b,Some tac,ipat,c) ->
-            hov 1 (
-              primitive (if b then "assert" else "enough") ++
-                pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
-                pr_by_tactic (pr.pr_tactic ltop) tac
-            )
-          | TacAssert (_,None,ipat,c) ->
-            hov 1 (
-              primitive "pose proof"
-              ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
-            )
-          | TacGeneralize l ->
-            hov 1 (
-              primitive "generalize" ++ spc ()
-              ++ prlist_with_sep pr_comma (fun (cl,na) ->
-                pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
-                l
-            )
-          | TacGeneralizeDep c ->
-            hov 1 (
-              primitive "generalize" ++ spc () ++ str "dependent"
-              ++ pr_constrarg c
-            )
-          | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
-            hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
-          | TacLetTac (na,c,cl,b,e) ->
-            hov 1 (
-              (if b then primitive "set" else primitive "remember") ++
-                (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
-                 else pr_pose_as_style pr.pr_constr na c) ++
-                pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
-                pr_clauses (Some b) pr.pr_name cl)
-          (*  | TacInstantiate (n,c,ConclLocation ()) ->
-              hov 1 (str "instantiate" ++ spc() ++
-              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-              pr_lconstrarg c ++ str ")" ))
-              | TacInstantiate (n,c,HypLocation (id,hloc)) ->
-              hov 1 (str "instantiate" ++ spc() ++
-              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-              pr_lconstrarg c ++ str ")" )
-              ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
-          *)
-
-          (* Derived basic tactics *)
-          | TacInductionDestruct (isrec,ev,(l,el)) ->
-            hov 1 (
-              primitive (with_evars ev (if isrec then "induction" else "destruct"))
-              ++ spc ()
-              ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
-                pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
-                  pr_with_induction_names pr.pr_dconstr ids ++
-                  pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
-                pr_opt pr_eliminator el
-            )
-          | TacDoubleInduction (h1,h2) ->
-            hov 1 (
-              primitive "double induction"
-              ++ pr_arg pr_quantified_hypothesis h1
-              ++ pr_arg pr_quantified_hypothesis h2
-            )
 
-          (* Automation tactics *)
-          | TacTrivial (_,[],Some []) as x ->
-            pr_atom0 x
-          | TacTrivial (d,lems,db) ->
-            hov 0 (
-              str (string_of_debug d) ++ primitive "trivial"
-              ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
-            )
-          | TacAuto (_,None,[],Some []) as x ->
-            pr_atom0 x
-          | TacAuto (d,n,lems,db) ->
-            hov 0 (
-              str (string_of_debug d) ++ primitive "auto"
-              ++ pr_opt (pr_or_var int) n
-              ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
-            )
+        (* Derived basic tactics *)
+        | TacInductionDestruct (isrec,ev,(l,el)) ->
+          hov 1 (
+            primitive (with_evars ev (if isrec then "induction" else "destruct"))
+            ++ spc ()
+            ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
+              pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
+                pr_with_induction_names pr.pr_dconstr ids ++
+                pr_opt (pr_clauses None pr.pr_name) cl) l ++
+              pr_opt pr_eliminator el
+          )
+        | TacDoubleInduction (h1,h2) ->
+          hov 1 (
+            primitive "double induction"
+            ++ pr_arg pr_quantified_hypothesis h1
+            ++ pr_arg pr_quantified_hypothesis h2
+          )
 
-          (* Context management *)
-          | TacClear (true,[]) as t ->
-            pr_atom0 t
-          | TacClear (keep,l) ->
-            hov 1 (
-              primitive "clear" ++ spc ()
-              ++ (if keep then str "- " else mt ())
-              ++ prlist_with_sep spc pr.pr_name l
-            )
-          | TacClearBody l ->
-            hov 1 (
-              primitive "clearbody" ++ spc ()
-              ++ prlist_with_sep spc pr.pr_name l
-            )
-          | TacMove (id1,id2) ->
-            hov 1 (
-              primitive "move"
-              ++ brk (1,1) ++ pr.pr_name id1
-              ++ Miscprint.pr_move_location pr.pr_name id2
-            )
-          | TacRename l ->
-            hov 1 (
-              primitive "rename" ++ brk (1,1)
-              ++ prlist_with_sep
-                (fun () -> str "," ++ brk (1,1))
-                (fun (i1,i2) ->
-                  pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
-                l
-            )
+        (* Context management *)
+        | TacRename l ->
+          hov 1 (
+            primitive "rename" ++ brk (1,1)
+            ++ prlist_with_sep
+              (fun () -> str "," ++ brk (1,1))
+              (fun (i1,i2) ->
+                pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
+              l
+          )
 
-          (* Constructors *)
-          | TacSplit (ev,l) ->
-            hov 1 (
-              primitive (with_evars ev "exists")
-              ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l
-            )
+        (* Conversion *)
+        | TacReduce (r,h) ->
+          hov 1 (
+            pr_red_expr r
+            ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+          )
+        | TacChange (op,c,h) ->
+          hov 1 (
+            primitive "change" ++ brk (1,1)
+            ++ (
+              match op with
+                  None ->
+                    mt ()
+                | Some p ->
+                  pr.pr_pattern p ++ spc ()
+                  ++ keyword "with" ++ spc ()
+            ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+          )
 
-          (* Conversion *)
-          | TacReduce (r,h) ->
-            hov 1 (
-              pr_red_expr r
-              ++ pr_clauses (Some true) pr.pr_name h
-            )
-          | TacChange (op,c,h) ->
-            hov 1 (
-              primitive "change" ++ brk (1,1)
-              ++ (
-                match op with
-                    None ->
-                      mt ()
-                  | Some p ->
-                    pr.pr_pattern p ++ spc ()
-                    ++ keyword "with" ++ spc ()
-              ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h
+        (* Equality and inversion *)
+        | TacRewrite (ev,l,cl,by) ->
+          hov 1 (
+            primitive (with_evars ev "rewrite") ++ spc ()
+            ++ prlist_with_sep
+              (fun () -> str ","++spc())
+              (fun (b,m,c) ->
+                pr_orient b ++ pr_multi m ++
+                  pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+              l
+            ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
+            ++ (
+              match by with
+                | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
+                | None -> mt()
             )
+          )
+        | TacInversion (DepInversion (k,c,ids),hyp) ->
+          hov 1 (
+            primitive "dependent " ++ pr_induction_kind k ++ spc ()
+            ++ pr_quantified_hypothesis hyp
+            ++ pr_with_inversion_names pr.pr_dconstr ids
+            ++ pr_with_constr pr.pr_constr c
+          )
+        | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+          hov 1 (
+            pr_induction_kind k ++ spc ()
+            ++ pr_quantified_hypothesis hyp
+            ++ pr_with_inversion_names pr.pr_dconstr ids
+            ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+          )
+        | TacInversion (InversionUsing (c,cl),hyp) ->
+          hov 1 (
+            primitive "inversion" ++ spc()
+            ++ pr_quantified_hypothesis hyp ++ spc ()
+            ++ keyword "using" ++ spc () ++ pr.pr_constr c
+            ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+          )
+      )
+      in
+      pr_atom1
 
-          (* Equivalence relations *)
-          | TacSymmetry cls ->
-            primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls
-
-          (* Equality and inversion *)
-          | TacRewrite (ev,l,cl,by) ->
-            hov 1 (
-              primitive (with_evars ev "rewrite") ++ spc ()
-              ++ prlist_with_sep
-                (fun () -> str ","++spc())
-                (fun (b,m,c) ->
-                  pr_orient b ++ pr_multi m ++
-                    pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
-                l
-              ++ pr_clauses (Some true) pr.pr_name cl
-              ++ (
-                match by with
-                  | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
-                  | None -> mt()
-              )
-            )
-          | TacInversion (DepInversion (k,c,ids),hyp) ->
-            hov 1 (
-              primitive "dependent " ++ pr_induction_kind k ++ spc ()
-              ++ pr_quantified_hypothesis hyp
-              ++ pr_with_inversion_names pr.pr_dconstr ids
-              ++ pr_with_constr pr.pr_constr c
-            )
-          | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
-            hov 1 (
-              pr_induction_kind k ++ spc ()
-              ++ pr_quantified_hypothesis hyp
-              ++ pr_with_inversion_names pr.pr_dconstr ids
-              ++ pr_simple_hyp_clause pr.pr_name cl
-            )
-          | TacInversion (InversionUsing (c,cl),hyp) ->
-            hov 1 (
-              primitive "inversion" ++ spc()
-              ++ pr_quantified_hypothesis hyp ++ spc ()
-              ++ keyword "using" ++ spc () ++ pr.pr_constr c
-              ++ pr_simple_hyp_clause pr.pr_name cl
-            )
-        )
-        in
+    let make_pr_tac pr strip_prod_binders tag_atom tag =
 
+        let extract_binders = function
+          | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+          | body -> ([],body) in
         let rec pr_tac inherited tac =
           let return (doc, l) = (tag tac doc, l) in
           let (strm, prec) = return (match tac with
@@ -1234,7 +1122,7 @@ module Make
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
             | TacAtom (loc,t) ->
-              pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
+              pr_with_comments loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
             | TacArg(_,Tacexp e) ->
               pr.pr_tactic (latom,E) e, latom
             | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
@@ -1257,26 +1145,17 @@ module Make
             | TacML (loc,s,l) ->
               pr_with_comments loc (pr.pr_extend 1 s l), lcall
             | TacAlias (loc,kn,l) ->
-              pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
+              pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
           )
           in
           if prec_less prec inherited then strm
           else str"(" ++ strm ++ str")"
 
         and pr_tacarg = function
-          | TacDynamic (loc,t) ->
-            pr_with_comments loc
-              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
-          | MetaIdArg (loc,true,s) ->
-            pr_with_comments loc (str "$" ++ str s)
-          | MetaIdArg (loc,false,s) ->
-            pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
             pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
-          | UConstr c ->
-            keyword "uconstr:" ++ pr.pr_uconstr c
           | TacFreshId l ->
             keyword "fresh" ++ pr_fresh_ids l
           | TacPretype c ->
@@ -1304,7 +1183,6 @@ module Make
     let pr = {
       pr_tactic = pr_raw_tactic_level;
       pr_constr = pr_constr_expr;
-      pr_uconstr = pr_constr_expr;
       pr_dconstr = pr_constr_expr;
       pr_lconstr = pr_lconstr_expr;
       pr_pattern = pr_constr_pattern_expr;
@@ -1312,8 +1190,8 @@ module Make
       pr_constant = pr_or_by_notation pr_reference;
       pr_reference = pr_reference;
       pr_name = pr_lident;
-      pr_generic = Genprint.generic_raw_print;
-      pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+      pr_generic = pr_raw_generic_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference;
+      pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
       pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
     } in
     make_pr_tac
@@ -1327,7 +1205,7 @@ module Make
 
   let pr_pat_and_constr_expr pr ((c,_),_) = pr c
 
-  let rec pr_glob_tactic_level env n t =
+  let pr_glob_tactic_level env n t =
     let glob_printers =
       (strip_prod_binders_glob_constr)
     in
@@ -1335,7 +1213,6 @@ module Make
       let pr = {
         pr_tactic = prtac;
         pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
-        pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
         pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
@@ -1343,8 +1220,10 @@ module Make
         pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
-        pr_generic = Genprint.generic_glb_print;
-        pr_extend = pr_glob_extend
+        pr_generic = pr_glb_generic_rec
+          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_extend = pr_glob_extend_rec
           (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
           prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
         pr_alias = pr_glob_alias
@@ -1369,15 +1248,11 @@ module Make
           | _ -> error "Cannot translate fix tactic: not enough products" in
     strip_ty [] n ty
 
-  let pr_tactic_level env n t =
-    let typed_printers =
-      (strip_prod_binders_constr)
-    in
-    let prtac n (t:tactic_expr) =
+  let pr_atomic_tactic_level env n t =
+    let prtac n (t:atomic_tactic_expr) =
       let pr = {
-        pr_tactic = pr_glob_tactic_level env;
+        pr_tactic = (fun _ _ -> str "<tactic>");
         pr_constr = pr_constr_env env Evd.empty;
-        pr_uconstr = pr_closed_glob_env env Evd.empty;
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_lconstr_env env Evd.empty;
         pr_pattern = pr_constr_pattern_env env Evd.empty;
@@ -1385,23 +1260,50 @@ module Make
         pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
-        pr_generic = Genprint.generic_top_print;
-        pr_extend = pr_extend
-          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-          (pr_glob_tactic_level env) pr_constr_pattern;
-        pr_alias = pr_alias
-          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-          (pr_glob_tactic_level env) pr_constr_pattern;
+        (** Those are not used by the atomic printer *)
+        pr_generic = (fun _ -> assert false);
+        pr_extend = (fun _ _ _ -> assert false);
+        pr_alias = (fun _ _ _ -> assert false);
       }
       in
-      make_pr_tac
-        pr typed_printers
-        tag_atomic_tactic_expr tag_tactic_expr
-        n t
+      pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
     in
     prtac n t
 
-  let pr_tactic env = pr_tactic_level env ltop
+  let pr_raw_generic env = pr_raw_generic_rec
+    pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference
+
+  let pr_glb_generic env = pr_glb_generic_rec
+    (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+    (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+  let pr_top_generic env = pr_top_generic_rec
+    (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+    pr_value pr_constr_pattern
+
+  let pr_raw_extend env = pr_raw_extend_rec
+    pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+
+  let pr_glob_extend env = pr_glob_extend_rec
+    (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+    (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+  let check_val_type t arg =
+    let ArgumentType t = t in
+(*     let t = Genarg.val_tag (Obj.magic t) in *)
+(*     let Val.Dyn (t', _) = arg in *)
+(*     match Genarg.Val.eq t t' with *)
+(*     | None -> false *)
+(*     | Some _ -> true *)
+    true (** FIXME *)
+
+  let pr_alias pr lev key args =
+    pr_alias_gen check_val_type pr lev key args
+
+  let pr_extend pr lev ml args =
+    pr_extend_gen check_val_type pr lev ml args
+
+  let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
 
 end
 
@@ -1431,23 +1333,31 @@ include Make (Ppconstr) (struct
     let tag_glob_atomic_tactic_expr = do_not_tag
     let tag_raw_tactic_expr         = do_not_tag
     let tag_raw_atomic_tactic_expr  = do_not_tag
-    let tag_tactic_expr             = do_not_tag
     let tag_atomic_tactic_expr      = do_not_tag
 end)
 
 (** Registering *)
 
+let run_delayed c =
+  Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
   let pr_string s = str "\"" ++ str s ++ str "\"" in
+  Genprint.register_print0 Constrarg.wit_int_or_var
+    (pr_or_var int) (pr_or_var int) int;
   Genprint.register_print0 Constrarg.wit_ref
     pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+  Genprint.register_print0 Constrarg.wit_ident
+    pr_id pr_id pr_id;
+  Genprint.register_print0 Constrarg.wit_var
+    (pr_located pr_id) (pr_located pr_id) pr_id;
   Genprint.register_print0
     Constrarg.wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty))));
+    (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
   Genprint.register_print0
     Constrarg.wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
@@ -1457,11 +1367,41 @@ let () =
   Genprint.register_print0 Constrarg.wit_sort
     pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
   Genprint.register_print0
+    Constrarg.wit_constr
+    Ppconstr.pr_constr_expr
+    (fun (c, _) -> Printer.pr_glob_constr c)
+    Printer.pr_constr
+  ;
+  Genprint.register_print0
     Constrarg.wit_uconstr
     Ppconstr.pr_constr_expr
     (fun (c,_) -> Printer.pr_glob_constr c)
     Printer.pr_closed_glob
   ;
+  Genprint.register_print0
+    Constrarg.wit_open_constr
+    Ppconstr.pr_constr_expr
+    (fun (c, _) -> Printer.pr_glob_constr c)
+    Printer.pr_constr
+  ;
+  Genprint.register_print0 Constrarg.wit_red_expr
+    (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
+    (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
+    (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
+  Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+  Genprint.register_print0 Constrarg.wit_bindings
+    (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
+    (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+  Genprint.register_print0 Constrarg.wit_constr_may_eval
+    (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
+    (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)
+      (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr))
+    pr_constr;
+  Genprint.register_print0 Constrarg.wit_constr_with_bindings
+    (pr_with_bindings pr_constr_expr pr_lconstr_expr)
+    (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
   Genprint.register_print0 Stdarg.wit_int int int int;
   Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
   Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
@@ -1472,16 +1412,10 @@ let () =
   let printer _ _ prtac = prtac (0, E) in
   declare_extra_genarg_pprule wit_tactic printer printer printer
 
-let _ = Hook.set Tactic_debug.tactic_printer
-  (fun x -> pr_glob_tactic (Global.env()) x)
-
-let _ = Hook.set Tactic_debug.match_pattern_printer
-  (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp)
-
-let _ = Hook.set Tactic_debug.match_rule_printer
-  (fun rl ->
-    pr_match_rule false (pr_glob_tactic (Global.env()))
-      (fun (_,p) -> pr_constr_pattern p) rl)
+let () =
+  let pr_unit _ _ _ () = str "()" in
+  let printer _ _ prtac = prtac (0, E) in
+  declare_extra_genarg_pprule wit_ltac printer printer pr_unit
 
 module Richpp = struct
 
@@ -1496,7 +1430,6 @@ module Richpp = struct
     let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a)
     let tag_raw_tactic_expr         e = tag (ARawTacticExpr e)
     let tag_raw_atomic_tactic_expr  a = tag (ARawAtomicTacticExpr a)
-    let tag_tactic_expr             e = tag (ATacticExpr e)
     let tag_atomic_tactic_expr      a = tag (AAtomicTacticExpr a)
   end)
 
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 30b9483db7..31a5a5d4a8 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -32,7 +32,7 @@ type 'a glob_extra_genarg_printer =
 type 'a extra_genarg_printer =
     (Term.constr -> std_ppcmds) ->
     (Term.constr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
 val declare_extra_genarg_pprule :
@@ -41,11 +41,11 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
-type grammar_terminals = string option list
+type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
-  pptac_args : argument_type list;
-  pptac_prods : int * grammar_terminals;
+  pptac_level : int;
+  pptac_prods : grammar_terminals;
 }
 
 val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 1631bda377..d4858bac4f 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,11 +8,9 @@
 
 open Pp
 open Genarg
-open Constrexpr
 open Tacexpr
 open Ppextend
 open Environ
-open Pattern
 open Misctypes
 
 module type Pp = sig
@@ -32,46 +30,24 @@ module type Pp = sig
 
   val pr_clauses :  bool option ->
     ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-  val pr_raw_generic :
-    (constr_expr -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) ->
-    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) ->
-    (Libnames.reference -> std_ppcmds) -> rlevel generic_argument ->
-    std_ppcmds
-
-  val pr_glb_generic :
-    (glob_constr_and_expr -> Pp.std_ppcmds) ->
-    (glob_constr_and_expr -> Pp.std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    (glob_constr_pattern_and_expr -> std_ppcmds) ->
-    glevel generic_argument -> std_ppcmds
-
-  val pr_top_generic :
-    (Term.constr -> std_ppcmds) ->
-    (Term.constr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    (Pattern.constr_pattern -> std_ppcmds) ->
-    tlevel generic_argument ->
-    std_ppcmds
-
-  val pr_raw_extend:
-    (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
-    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) -> int ->
-    ml_tactic_entry -> raw_generic_argument list -> std_ppcmds
-
-  val pr_glob_extend:
-    (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
-    ml_tactic_entry -> glob_generic_argument list -> std_ppcmds
+
+  val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+  val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+  val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds
+
+  val pr_raw_extend: env -> int ->
+    ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+  val pr_glob_extend: env -> int ->
+    ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
 
   val pr_extend :
-    (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    (constr_pattern -> std_ppcmds) -> int ->
-    ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
+    (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+  val pr_alias : (Val.t -> std_ppcmds) ->
+    int -> Names.KerName.t -> Val.t list -> std_ppcmds
 
   val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
 
@@ -81,7 +57,7 @@ module type Pp = sig
 
   val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
 
-  val pr_tactic : env -> tactic_expr -> std_ppcmds
+  val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
 
   val pr_hintbases : string list option -> std_ppcmds
 
@@ -91,4 +67,11 @@ module type Pp = sig
     ('constr -> std_ppcmds) ->
     ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
 
+  val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+  val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+    ('b, 'a) match_rule -> std_ppcmds
+
+  val pr_value : tolerability -> Val.t -> std_ppcmds
+
 end
diff --git a/printing/pputils.ml b/printing/pputils.ml
index ee1a39efd3..906b463a85 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 7287748327..a0f2c77283 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4e889e55f0..f0548238a7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -43,6 +43,12 @@ module Make
     else
       pr_id id
 
+  let pr_plident (lid, l) =
+    pr_lident lid ++
+    (match l with
+     | Some l -> prlist_with_sep spc pr_lident l
+     | None -> mt())
+    
   let string_of_fqid fqid =
     String.concat "." (List.map Id.to_string fqid)
 
@@ -73,13 +79,7 @@ module Make
     | VernacEndSubproof -> str""
     | _ -> str"."
 
-  let pr_gen t =
-    pr_raw_generic
-      pr_constr_expr
-      pr_lconstr_expr
-      pr_raw_tactic_level
-      pr_constr_expr
-      pr_reference t
+  let pr_gen t = pr_raw_generic (Global.env ()) t
 
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
@@ -104,13 +104,6 @@ module Make
     if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
     else id
 
-  let pr_production_item = function
-    | TacNonTerm (loc,nt,Some (p,sep)) ->
-      let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
-      str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
-    | TacNonTerm (loc,nt,None) -> str nt
-    | TacTerm s -> qs s
-
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
     | CommentString s -> qs s
@@ -160,6 +153,8 @@ module Make
     (* This should not happen because of the grammar *)
       | IntValue (Some n) -> spc() ++ int n
       | StringValue s -> spc() ++ str s
+      | StringOptValue None -> mt()
+      | StringOptValue (Some s) -> spc() ++ str s
       | BoolValue b -> mt()
     in pr_printoption a None ++ pr_opt_value b
 
@@ -348,6 +343,7 @@ module Make
       | l ->
         prlist_with_sep spc
           (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+
 (*
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
@@ -376,21 +372,16 @@ module Make
     | l -> spc() ++
       hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-  let print_level n =
-    if not (Int.equal n 0) then
-      spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")")
-    else
-      mt ()
-
-  let pr_grammar_tactic_rule n (_,pil,t) =
-    hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++
-             hov 0 (prlist_with_sep sep pr_production_item pil ++
-                      spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
+  let pr_univs pl =
+    match pl with
+    | None -> mt ()
+    | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
 
-  let pr_statement head (id,(bl,c,guard)) =
-    assert (not (Option.is_empty id));
+  let pr_statement head (idpl,(bl,c,guard)) =
+    assert (not (Option.is_empty idpl));
+    let id, pl = Option.get idpl in
     hov 2
-      (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
+      (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
          pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
@@ -458,8 +449,6 @@ module Make
         keyword "Print TypeClasses"
       | PrintInstances qid ->
         keyword "Print Instances" ++ spc () ++ pr_smart_global qid
-      | PrintLtac qid ->
-        keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid
       | PrintCoercions ->
         keyword "Print Coercions"
       | PrintCoercionPaths (s,t) ->
@@ -478,8 +467,6 @@ module Make
         keyword "Print Hint *"
       | PrintHintDbName s ->
         keyword "Print HintDb" ++ spc () ++ str s
-      | PrintRewriteHintDbName s ->
-        keyword "Print Rewrite HintDb" ++ spc() ++ str s
       | PrintUniverses (b, fopt) ->
         let cmd =
           if b then "Print Sorted Universes"
@@ -579,7 +566,8 @@ module Make
           let pr_goal_reference = function
             | OpenSubgoals -> mt ()
             | NthGoal n -> spc () ++ int n
-            | GoalId n -> spc () ++ str n in
+            | GoalId id -> spc () ++ pr_id id
+            | GoalUid n -> spc () ++ str n in
           let pr_showable = function
             | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
             | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
@@ -625,10 +613,10 @@ module Make
               else
                 spc() ++ qs s
           )
-        | VernacTime v ->
-          return (keyword "Time" ++ spc() ++ pr_vernac_list v)
-        | VernacRedirect (s, v) ->
-          return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
+        | VernacTime (_,v) ->
+          return (keyword "Time" ++ spc() ++ pr_vernac v)
+        | VernacRedirect (s, (_,v)) ->
+          return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v)
         | VernacTimeout(n,v) ->
           return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
         | VernacFail v ->
@@ -637,8 +625,6 @@ module Make
           return (keyword "No-parsing-rule for VernacError")
 
       (* Syntax *)
-        | VernacTacticNotation (n,r,e) ->
-          return (pr_grammar_tactic_rule n ("",r,e))
         | VernacOpenCloseScope (_,(opening,sc)) ->
           return (
             keyword (if opening then "Open " else "Close ") ++
@@ -656,7 +642,7 @@ module Make
         | VernacBindScope (sc,cll) ->
           return (
             keyword "Bind Scope" ++ spc () ++ str sc ++
-              spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll
+              spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
           )
         | VernacArgumentsScope (q,scl) ->
           let pr_opt_scope = function
@@ -729,7 +715,7 @@ module Make
           return (
             hov 2 (
               pr_def_token d ++ spc()
-              ++ pr_lident id ++ binds ++ typ
+              ++ pr_plident id ++ binds ++ typ
               ++ (match c with
                 | None -> mt()
                 | Some cc -> str" :=" ++ spc() ++ cc))
@@ -760,11 +746,12 @@ module Make
           return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
         | VernacAssumption (stre,_,l) ->
           let n = List.length (List.flatten (List.map fst (List.map snd l))) in
-          return (
-            hov 2
-              (pr_assumption_token (n > 1) stre ++ spc() ++
-                 pr_ne_params_list pr_lconstr_expr l)
-          )
+          let pr_params (c, (xl, t)) =
+            hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++
+              (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t))
+          in
+          let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
+          return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions))
         | VernacInductive (p,f,l) ->
           let pr_constructor (coe,(id,c)) =
             hov 2 (pr_lident id ++ str" " ++
@@ -781,12 +768,12 @@ module Make
             | RecordDecl (c,fs) ->
               pr_record_decl b c fs
           in
-          let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+          let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
             hov 0 (
               str key ++ spc() ++
-                (if coe then str"> " else str"") ++ pr_lident id ++
-                pr_and_type_binders_arg indpar ++ spc() ++
-                Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
+                (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
+                pr_and_type_binders_arg indpar ++
+                pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
                 str" :=") ++ pr_constructor_list k lc ++
               prlist (pr_decl_notation pr_constr) ntn
           in
@@ -808,9 +795,9 @@ module Make
             | None | Some Global -> ""
           in
           let pr_onerec = function
-            | ((loc,id),ro,bl,type_,def),ntn ->
+            | (((loc,id),pl),ro,bl,type_,def),ntn ->
               let annot = pr_guard_annot pr_lconstr_expr bl ro in
-              pr_id id ++ pr_binders_arg bl ++ annot
+              pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
               ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
               ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
                 prlist (pr_decl_notation pr_constr) ntn
@@ -826,8 +813,8 @@ module Make
             | Some Local -> keyword "Local" ++ spc ()
             | None | Some Global -> str ""
           in
-          let pr_onecorec (((loc,id),bl,c,def),ntn) =
-            pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+          let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
+            pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
               spc() ++ pr_lconstr_expr c ++
               pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
               prlist (pr_decl_notation pr_constr) ntn
@@ -908,8 +895,9 @@ module Make
             hov 1 (
               (if abst then keyword "Declare" ++ spc () else mt ()) ++
                 keyword "Instance" ++
-                (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
-                    Anonymous -> mt ()) ++
+                (match instid with
+		 | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () 
+                 | (_, Anonymous), _ -> mt ()) ++
                 pr_and_type_binders_arg sup ++
                 str":" ++ spc () ++
                 pr_constr cl ++ pr_priority pri ++
@@ -970,24 +958,6 @@ module Make
                      prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
           )
         (* Solving *)
-      | VernacSolve (i,info,tac,deftac) ->
-        let pr_goal_selector = function
-          | SelectNth i -> int i ++ str":"
-          | SelectId id -> pr_id id ++ str":"
-          | SelectAll -> str"all" ++ str":"
-          | SelectAllParallel -> str"par"
-        in
-        let pr_info =
-          match info with
-            | None -> mt ()
-            | Some i -> str"Info"++spc()++int i++spc()
-        in
-        return (
-          (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
-          pr_info ++
-          pr_raw_tactic tac
-          ++ (if deftac then str ".." else mt ())
-        )
         | VernacSolveExistential (i,c) ->
           return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
 
@@ -1019,24 +989,6 @@ module Make
           return (keyword "Cd" ++ pr_opt qs s)
 
         (* Commands *)
-        | VernacDeclareTacticDefinition (rc,l) ->
-          let pr_tac_body (id, redef, body) =
-            let idl, body =
-              match body with
-                | Tacexpr.TacFun (idl,b) -> idl,b
-                | _ -> [], body in
-            pr_ltac_ref id ++
-              prlist (function None -> str " _"
-                | Some id -> spc () ++ pr_id id) idl
-            ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
-              pr_raw_tactic body
-          in
-          return (
-            hov 1
-              (keyword "Ltac" ++ spc () ++
-                 prlist_with_sep (fun () ->
-                   fnl() ++ keyword "with" ++ spc ()) pr_tac_body l)
-          )
         | VernacCreateHintDb (dbname,b) ->
           return (
             hov 1 (keyword "Create HintDb" ++ spc () ++
@@ -1213,8 +1165,6 @@ module Make
               (keyword "Comments" ++ spc()
                ++ prlist_with_sep sep (pr_comment pr_constr) l)
           )
-        | VernacNop ->
-          mt()
 
         (* Toplevel control *)
         | VernacToplevelControl exn ->
@@ -1251,33 +1201,21 @@ module Make
         | VernacEndSubproof ->
           return (str "}")
 
-    and pr_vernac_list l =
-      hov 2 (str"[" ++ spc() ++
-               prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
-             ++ spc() ++ str"]")
-
     and pr_extend s cl =
       let pr_arg a =
         try pr_gen a
         with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
       try
         let rl = Egramml.get_extend_vernac_rule s in
-        let start,rl,cl =
-          match rl with
-            | Egramml.GramTerminal s :: rl -> str s, rl, cl
-            | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
-            | [] -> anomaly (Pp.str "Empty entry") in
-        let (pp,_) =
-          List.fold_left
-            (fun (strm,args) pi ->
-              let pp,args = match pi with
-                | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
-                | Egramml.GramTerminal s -> (str s, args) in
-              (strm ++ spc() ++ pp), args)
-            (start,cl) rl in
-        hov 1 pp
+        let rec aux rl cl =
+          match rl, cl with
+          | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+          | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+          | [], [] -> []
+          | _ -> assert false in
+        hov 1 (pr_sequence (fun x -> x) (aux rl cl))
       with Not_found ->
-        hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+        hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
     in pr_vernac
 
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index f38848cdcf..d3d4a5ceb7 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
index cfcd49744e..5d1c89332c 100644
--- a/printing/ppvernacsig.mli
+++ b/printing/ppvernacsig.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b8c5fd4cfc..9745a79250 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -35,7 +35,7 @@ type object_pr = {
   print_syntactic_def       : kernel_name -> std_ppcmds;
   print_module              : bool -> Names.module_path -> std_ppcmds;
   print_modtype             : module_path -> std_ppcmds;
-  print_named_decl          : Id.t * constr option * types -> std_ppcmds;
+  print_named_decl          : Context.Named.Declaration.t -> std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
@@ -73,8 +73,15 @@ let print_ref reduce ref =
       in it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
-  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ 
-  	   Printer.pr_universe_ctx univs)
+  let env = Global.env () in
+  let bl = Universes.universe_binders_of_global ref in
+  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
+  let inst =
+    if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
+    else mt ()
+  in
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ 
+  	   Printer.pr_universe_ctx sigma univs)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -125,7 +132,8 @@ let print_renames_list prefix l =
 let need_expansion impl ref =
   let typ = Global.type_of_global_unsafe ref in
   let ctx = prod_assum typ in
-  let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in
+  let open Context.Rel.Declaration in
+  let nprods = List.count is_local_assum ctx in
   not (List.is_empty impl) && List.length impl >= nprods &&
     let _,lastimpl = List.chop nprods impl in
       List.exists is_status_implicit lastimpl
@@ -161,8 +169,10 @@ type opacity =
   | FullyOpaque
   | TransparentMaybeOpacified of Conv_oracle.level
 
-let opacity env = function
-  | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) ->
+let opacity env =
+  let open Context.Named.Declaration in
+  function
+  | VarRef v when is_local_def (Environ.lookup_named v env) ->
       Some(TransparentMaybeOpacified
         (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v)))
   | ConstRef cst ->
@@ -208,8 +218,8 @@ let print_polymorphism ref =
 let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
     let eta = match recflag with
-    | Decl_kinds.CoFinite -> mt ()
-    | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+    | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+    | Decl_kinds.BiFinite -> str " and has eta conversion"
     in
     [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
   | _ -> []
@@ -433,11 +443,13 @@ let print_named_def name body typ =
 let print_named_assum name typ =
   str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
 
-let gallina_print_named_decl (id,c,typ) =
-  let s = Id.to_string id in
-  match c with
-    | Some body -> print_named_def s body typ
-    | None -> print_named_assum s typ
+let gallina_print_named_decl =
+  let open Context.Named.Declaration in
+  function
+  | LocalAssum (id, typ) ->
+     print_named_assum (Id.to_string id) typ
+  | LocalDef (id, body, typ) ->
+     print_named_def (Id.to_string id) body typ
 
 let assumptions_for_print lna =
   List.fold_right (fun na env -> add_name na env) lna empty_names_context
@@ -463,16 +475,21 @@ let gallina_print_section_variable id =
   print_named_decl id ++
   with_line_skip (print_name_infos (VarRef id))
 
-let print_body = function
-  | Some c  -> pr_lconstr c
+let print_body env evd = function
+  | Some c  -> pr_lconstr_env env evd c
   | None -> (str"<no body>")
 
-let print_typed_body (val_0,typ) =
-  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ)
+let print_typed_body env evd (val_0,typ) =
+  (print_body env evd val_0 ++ fnl () ++ str "     : " ++ pr_ltype_env env evd typ)
 
 let ungeneralized_type_of_constant_type t = 
   Typeops.type_of_constant_type (Global.env ()) t
 
+let print_instance sigma cb =
+  if cb.const_polymorphic then
+    pr_universe_instance sigma cb.const_universes
+  else mt()
+				
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
@@ -481,17 +498,23 @@ let print_constant with_values sep sp =
   let univs = Univ.instantiate_univ_context 
     (Global.universes_of_constant_body cb)
   in
+  let ctx =
+    Evd.evar_universe_context_of_binders
+      (Universes.universe_binders_of_global (ConstRef sp))
+  in
+  let env = Global.env () and sigma = Evd.from_ctx ctx in
+  let pr_ltype = pr_ltype_env env sigma in
   hov 0 (pr_polymorphic cb.const_polymorphic ++
     match val_0 with
     | None ->
 	str"*** [ " ++
-	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
+	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_universe_ctx univs
+	Printer.pr_universe_ctx sigma univs
     | _ ->
-	print_basename sp ++ str sep ++ cut () ++
-	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
-        Printer.pr_universe_ctx univs)
+	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
+	(if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++
+        Printer.pr_universe_ctx sigma univs)
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
@@ -703,8 +726,8 @@ let print_any_name = function
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
     if not (DirPath.is_empty dir) then raise Not_found;
-    let (_,c,typ) = Global.lookup_named str in
-    (print_named_decl (str,c,typ))
+    let open Context.Named.Declaration in
+    str |> Global.lookup_named |> set_id str |> print_named_decl
   with Not_found ->
     errorlabstrm
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
@@ -732,8 +755,8 @@ let print_opaque_name qid =
 	let ty = Universes.unsafe_type_of_global gr in
 	print_typed_value (mkConstruct cstr, ty)
     | VarRef id ->
-        let (_,c,ty) = lookup_named id env in
-	print_named_decl (id,c,ty)
+        let open Context.Named.Declaration in
+        lookup_named id env |> set_id id |> print_named_decl
 
 let print_about_any loc k =
   match k with
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 6216d4d531..0eab155796 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -66,7 +66,7 @@ type object_pr = {
   print_syntactic_def       : kernel_name -> std_ppcmds;
   print_module              : bool -> Names.module_path -> std_ppcmds;
   print_modtype             : module_path -> std_ppcmds;
-  print_named_decl          : Id.t * constr option * types -> std_ppcmds;
+  print_named_decl          : Context.Named.Declaration.t -> std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
diff --git a/printing/printer.ml b/printing/printer.ml
index 33b95c2f56..22bc122bd5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -30,7 +30,8 @@ let delayed_emacs_cmd s =
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
-    (Evd.empty, Global.env())
+    let env = Global.env () in
+    (Evd.from_env env, env)
 
 (**********************************************************************)
 (** Terms                                                             *)
@@ -50,7 +51,7 @@ let pr_lconstr_core goal_concl_style env sigma t =
 
 let pr_lconstr_env env = pr_lconstr_core false env
 let pr_constr_env env = pr_constr_core false env
-let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env
+let _ = Hook.set Refine.pr_constr pr_constr_env
 
 let pr_lconstr_goal_style_env env = pr_lconstr_core true env
 let pr_constr_goal_style_env env = pr_constr_core true env
@@ -208,10 +209,10 @@ let safe_pr_constr t =
   let (sigma, env) = get_current_context () in
   safe_pr_constr_env env sigma t
 
-let pr_universe_ctx c =
+let pr_universe_ctx sigma c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context Universes.pr_with_global_universes c)) c
+      (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c
   else
     mt()
 
@@ -262,16 +263,19 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) =
   let ptyp = (str" : " ++ pt) in
   (pr_id id ++ hov 0 (pbody ++ ptyp))
 
-let pr_var_decl env sigma (id,c,typ) =
-  pr_var_decl_skel pr_id env sigma (id,c,typ)
+let pr_var_decl env sigma d =
+  pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d)
 
 let pr_var_list_decl env sigma (l,c,typ) =
   hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ))
 
-let pr_rel_decl env sigma (na,c,typ) =
-  let pbody = match c with
-    | None -> mt ()
-    | Some c ->
+let pr_rel_decl env sigma decl =
+  let open Context.Rel.Declaration in
+  let na = get_name decl in
+  let typ = get_type decl in
+  let pbody = match decl with
+    | LocalAssum _ -> mt ()
+    | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = pr_lconstr_env env sigma c in
 	let pb = if isCast c then surround pb else pb in
@@ -293,7 +297,7 @@ let pr_named_context_of env sigma =
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
 let pr_named_context env sigma ne_context =
-  hv 0 (Context.fold_named_context
+  hv 0 (Context.Named.fold_outside
 	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
           ne_context ~init:(mt ()))
 
@@ -306,7 +310,7 @@ let pr_rel_context_of env sigma =
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited env sigma =
   let sign_env =
-    Context.fold_named_list_context
+    Context.NamedList.fold
       (fun d pps ->
          let pidt =  pr_var_list_decl env sigma d in
          (pps ++ fnl () ++ pidt))
@@ -333,7 +337,7 @@ let pr_context_limit n env sigma =
   else
     let k = lgsign-n in
     let _,sign_env =
-      Context.fold_named_list_context
+      Context.NamedList.fold
         (fun d (i,pps) ->
            if i < k then
 	     (i+1, (pps ++str "."))
@@ -400,7 +404,7 @@ let display_name = false
 
 (* display a goal name *)
 let pr_goal_name sigma g =
-  if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
+  if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
   else mt ()
 
 (* display the conclusion of a goal *)
@@ -420,7 +424,8 @@ let pr_evgl_sign sigma evi =
   | None -> [], []
   | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi)
   in
-  let ids = List.rev_map pi1 l in
+  let open Context.Named.Declaration in
+  let ids = List.rev_map get_id l in
   let warn =
     if List.is_empty ids then mt () else
       (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
@@ -455,14 +460,17 @@ let pr_ne_evar_set hd tl sigma l =
   else
     mt ()
 
+let pr_selected_subgoal name sigma g =
+  let pg = default_pr_goal { sigma=sigma ; it=g; } in
+  v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g
+       ++ str " is:" ++ cut () ++ pg)
+
 let default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
     | g::rest ->
 	if Int.equal p 1 then
-          let pg = default_pr_goal { sigma=sigma ; it=g; } in
-          v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g 
-	       ++ str " is:" ++ cut () ++ pg)
+          pr_selected_subgoal (int n) sigma g
 	else
 	  prrec (p-1) rest
   in
@@ -636,8 +644,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
 	  | _ , _, _ ->
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
-	      (match Proof_global.Bullet.suggest p
-              with None  -> str"" | Some s -> fnl () ++ str s) ++
+              (let s = Proof_global.Bullet.suggest p in
+               if Pp.is_empty s then s else fnl () ++ s) ++
               fnl ()
             in
 	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
@@ -652,9 +660,17 @@ let pr_nth_open_subgoal n =
 
 let pr_goal_by_id id =
   let p = Proof_global.give_me_the_proof () in
-  let g = Goal.get_by_uid id in
+  try
+    Proof.in_proof p (fun sigma ->
+      let g = Evd.evar_key id sigma in
+      pr_selected_subgoal (pr_id id) sigma g)
+  with Not_found -> error "No such goal."
+
+let pr_goal_by_uid uid =
+  let p = Proof_global.give_me_the_proof () in
+  let g = Goal.get_by_uid uid in
   let pr gs =
-    v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut ()
+    v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut ()
 	 ++ pr_goal gs)
   in
   try
@@ -715,7 +731,7 @@ let prterm = pr_lconstr
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Axiom of constant * (Label.t * Context.Rel.t * types) list
   | Opaque of constant     (* An opaque constant. *)
   | Transparent of constant
 
@@ -724,25 +740,25 @@ module OrderedContextObject =
 struct
   type t = context_object
   let compare x y =
-      match x , y with
-      | Variable i1 , Variable i2 -> Id.compare i1 i2
-      | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
-      | Opaque k1 , Opaque k2 -> con_ord k1 k2
-      | Transparent k1 , Transparent k2 -> con_ord k1 k2
-      | Axiom _ , Variable _ -> 1
-      | Opaque _ , Variable _
-      | Opaque _ , Axiom _ -> 1
-      | Transparent _ , Variable _
-      | Transparent _ , Axiom _
-      | Transparent _ , Opaque _ -> 1
-      | _ , _ -> -1
+    match x , y with
+    | Variable i1 , Variable i2 -> Id.compare i1 i2
+    | Variable _ , _ -> -1
+    | _ , Variable _ -> 1
+    | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
+    | Axiom _ , _ -> -1
+    | _ , Axiom _ -> 1
+    | Opaque k1 , Opaque k2 -> con_ord k1 k2
+    | Opaque _ , _ -> -1
+    | _ , Opaque _ -> 1
+    | Transparent k1 , Transparent k2 -> con_ord k1 k2
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let pr_assumptionset env s =
-  if ContextObjectMap.is_empty s then
+  if ContextObjectMap.is_empty s &&
+       engagement env = (PredicativeSet, StratifiedType) then
     str "Closed under the global context"
   else
     let safe_pr_constant env kn =
@@ -765,7 +781,7 @@ let pr_assumptionset env s =
       let (v, a, o, tr) = accu in
       match t with
       | Variable id ->
-        let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
+        let var = pr_id id ++ str " : " ++ pr_ltype typ in
         (var :: v, a, o, tr)
       | Axiom (kn,[]) ->
         let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
@@ -774,7 +790,7 @@ let pr_assumptionset env s =
         let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++
           cut() ++
           prlist_with_sep cut (fun (lbl, ctx, ty) ->
-            str " used in " ++ str (Names.Label.to_string lbl) ++
+            str " used in " ++ pr_label lbl ++
             str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
           l in
         (v, ax :: a, o, tr)
@@ -788,6 +804,16 @@ let pr_assumptionset env s =
     let (vars, axioms, opaque, trans) = 
       ContextObjectMap.fold fold s ([], [], [], [])
     in
+    let theory =
+      if is_impredicative_set env then
+	[str "Set is impredicative"]
+      else []
+    in
+    let theory =
+      if type_in_type env then
+	str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
+      else theory
+    in
     let opt_list title = function
     | [] -> None
     | l ->
@@ -801,6 +827,7 @@ let pr_assumptionset env s =
       opt_list (str "Section Variables:") vars;
       opt_list (str "Axioms:") axioms;
       opt_list (str "Opaque constants:") opaque;
+      opt_list (str "Theory:") theory;
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
@@ -813,3 +840,7 @@ let pr_polymorphic b =
     if b then str"Polymorphic " else str"Monomorphic "
   else mt ()
 
+let pr_universe_instance evd ctx =
+  let inst = Univ.UContext.instance ctx in
+    str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
+
diff --git a/printing/printer.mli b/printing/printer.mli
index 5f56adbe6f..70993bb727 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,6 @@ open Pp
 open Names
 open Globnames
 open Term
-open Context
 open Environ
 open Pattern
 open Evd
@@ -84,7 +83,8 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 (** Universe constraints *)
 
 val pr_polymorphic         : bool -> std_ppcmds
-val pr_universe_ctx        : Univ.universe_context -> std_ppcmds
+val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
@@ -108,13 +108,13 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
 
-val pr_var_decl            : env -> evar_map -> named_declaration -> std_ppcmds
-val pr_var_list_decl       : env -> evar_map -> named_list_declaration -> std_ppcmds
-val pr_rel_decl            : env -> evar_map -> rel_declaration -> std_ppcmds
+val pr_var_decl            : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
+val pr_var_list_decl       : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
 
-val pr_named_context       : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context       : env -> evar_map -> Context.Named.t -> std_ppcmds
 val pr_named_context_of    : env -> evar_map -> std_ppcmds
-val pr_rel_context         : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context         : env -> evar_map -> Context.Rel.t -> std_ppcmds
 val pr_rel_context_of      : env -> evar_map -> std_ppcmds
 val pr_context_of          : env -> evar_map -> std_ppcmds
 
@@ -164,7 +164,7 @@ val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 type context_object =
   | Variable of Id.t  (** A section variable or a Let definition *)
   (** An axiom and the type it inhabits (if an axiom of the empty type) *)
-  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Axiom of constant * (Label.t * Context.Rel.t * types) list
   | Opaque of constant      (** An opaque constant. *)
   | Transparent of constant (** A transparent constant *)
 
@@ -175,7 +175,8 @@ module ContextObjectMap : CMap.ExtS
 val pr_assumptionset :
   env -> Term.types ContextObjectMap.t -> std_ppcmds
 
-val pr_goal_by_id : string -> std_ppcmds
+val pr_goal_by_id : Id.t -> std_ppcmds
+val pr_goal_by_uid : string -> std_ppcmds
 
 type printer_pr = {
  pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
diff --git a/printing/printmod.ml b/printing/printmod.ml
index a80bbb146a..9354cd28d0 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -72,10 +72,10 @@ let print_params env sigma params =
   if List.is_empty params then mt ()
   else Printer.pr_rel_context env sigma params ++ brk(1,2)
 
-let print_constructors envpar names types =
+let print_constructors envpar sigma names types =
   let pc =
     prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
-      (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c)
+      (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c)
       (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
   in
   hv 0 (str "  " ++ pc)
@@ -83,21 +83,26 @@ let print_constructors envpar names types =
 let build_ind_type env mip =
   Inductive.type_of_inductive env mip
 
-let print_one_inductive env mib ((_,i) as ind) =
+let print_one_inductive env sigma mib ((_,i) as ind) =
   let u = if mib.mind_polymorphic then 
       Univ.UContext.instance mib.mind_universes 
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
+  let args = Context.Rel.to_extended_list 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
   let envpar = push_rel_context params env in
+  let inst =
+    if mib.mind_polymorphic then
+      Printer.pr_universe_instance sigma mib.mind_universes
+    else mt ()
+  in
   hov 0 (
-    pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
-    str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
-  brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+    pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
+    str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
+  brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
 
 let print_mutual_inductive env mind mib =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
@@ -109,11 +114,13 @@ let print_mutual_inductive env mind mib =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
+  let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
+  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
     def keyword ++ spc () ++
     prlist_with_sep (fun () -> fnl () ++ str"  with ")
-      (print_one_inductive env mib) inds ++
-      Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+      (print_one_inductive env sigma mib) inds ++
+      Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -136,12 +143,14 @@ let print_record env mind mib =
   in
   let mip = mib.mind_packets.(0) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
+  let args = Context.Rel.to_extended_list 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
+  let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in
+  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let keyword =
     let open Decl_kinds in
     match mib.mind_finite with
@@ -153,16 +162,16 @@ let print_record env mind mib =
     hov 0 (
       Printer.pr_polymorphic mib.mind_polymorphic ++
       def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
-      print_params env Evd.empty params ++
-      str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++
+      print_params env sigma params ++
+      str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
       str ":= " ++ pr_id mip.mind_consnames.(0)) ++
     brk(1,2) ++
     hv 2 (str "{ " ++
       prlist_with_sep (fun () -> str ";" ++ brk(2,0))
         (fun (id,b,c) ->
           pr_id id ++ str (if b then " : " else " := ") ++
-          Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++
-      Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+      Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
 
 let pr_mutual_inductive_body env mind mib =
   if mib.mind_record <> None && not !Flags.raw_print then
@@ -254,11 +263,16 @@ let nametab_register_modparam mbid mtb =
       List.iter (nametab_register_body mp dir) struc
 
 let print_body is_impl env mp (l,body) =
-  let name = str (Label.to_string l) in
+  let name = pr_label l in
   hov 2 (match body with
     | SFBmodule _ -> keyword "Module" ++ spc () ++ name
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
     | SFBconst cb ->
+       let u =
+	 if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
+	 else Univ.Instance.empty
+       in
+       let sigma = Evd.empty in
       (match cb.const_body with
 	| Def _ -> def "Definition" ++ spc ()
 	| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
@@ -267,15 +281,17 @@ let print_body is_impl env mp (l,body) =
 	  | None -> mt ()
 	  | Some env ->
 	    str " :" ++ spc () ++
-	    hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *)
-		     (Typeops.type_of_constant_type env cb.const_type)) ++
+	    hov 0 (Printer.pr_ltype_env env sigma
+		(Vars.subst_instance_constr u
+   		  (Typeops.type_of_constant_type env cb.const_type))) ++
 	    (match cb.const_body with
 	      | Def l when is_impl ->
 		spc () ++
 		hov 2 (str ":= " ++
-		       Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l))
+		       Printer.pr_lconstr_env env sigma
+			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx cb.const_universes)
+	    Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes))
     | SFBmind mib ->
       try
 	let env = Option.get env in
diff --git a/printing/printmod.mli b/printing/printmod.mli
index bea4753451..7f7d343927 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
index 5d0d4ab0b4..f71fffdcec 100644
--- a/printing/printmodsig.mli
+++ b/printing/printmodsig.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d95e190749..5f39f36eab 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -22,4 +22,3 @@ let make_richpp pr ast =
 
 let richpp_vernac = make_richpp RichppVernac.pr_vernac
 let richpp_constr = make_richpp RichppConstr.pr_constr_expr
-let richpp_tactic env = make_richpp (RichppTactic.pr_tactic env)
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
index 41c313514b..c9e84e3eb4 100644
--- a/printing/richprinter.mli
+++ b/printing/richprinter.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -34,6 +34,3 @@ val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
 
 (** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
 val richpp_constr : Constrexpr.constr_expr -> rich_pp
-
-(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *)
-val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp