Restructuration printer et parser

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

13 files changed, 508 insertions, 899 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 7dad63a00..989b78638 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -286,7 +286,7 @@ let dbize k sigma =
     | Node(loc,"APPLIST", f::args) ->	   
 	RApp (loc,dbrec env f,List.map (dbrec env) args)
 	  
-    | Node(loc,"MULTCASE", p:: Node(_,"TOMATCH",tms):: eqns) ->
+    | Node(loc,"CASES", p:: Node(_,"TOMATCH",tms):: eqns) ->
 	let po = match p with 
 	  | Str(_,"SYNTH") -> None 
 	  | _ -> Some(dbrec env p) in
@@ -449,7 +449,7 @@ let globalize_ast ast =
 (* Installation of the AST quotations. "command" is used by default. *)
 let _ = 
   Pcoq.define_quotation true "command" 
-    (Pcoq.map_entry globalize_command Pcoq.Command.command)
+    (Pcoq.map_entry globalize_command Pcoq.Constr.constr)
 let _ = 
   Pcoq.define_quotation false "tactic" 
     (Pcoq.map_entry globalize_ast Pcoq.Tactic.tactic)
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 71edadb8f..c5be89d92 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -83,14 +83,13 @@ let add_rule whatfor se =
   from_name_table := Gmap.add name se !from_name_table;
   from_key_table := Gmapl.add key se !from_key_table
     
-let add_ppobject (wf,sel) = List.iter (add_rule wf) sel
+let add_ppobject {sc_univ=wf;sc_entries=sel} = List.iter (add_rule wf) sel
 
 
 (* Pretty-printing machinery *)
 
 type std_printer = Coqast.t -> std_ppcmds
-type unparsing_subfunction =
-    ((string * precedence) * parenRelation) option -> std_printer
+type unparsing_subfunction = string -> tolerability option -> std_printer
 
 (* Module of primitive printers *)
 module Ppprim =
@@ -124,19 +123,17 @@ let _ = Ppprim.add ("print_as",print_as_printer)
  * printed using the token_printer, unless another primitive printer
  * is specified. *)
 
-let print_syntax_entry sub_pr env se = 
+let print_syntax_entry whatfor sub_pr env se = 
   let rule_prec = (se.syn_id, se.syn_prec) in
   let rec print_hunk = function
-    | PH(e,pprim,reln) ->
-        let sub_printer = sub_pr (Some(rule_prec,reln)) in
+    | PH(e,externpr,reln) ->
         let printer =
-          match pprim with (* If a primitive printer is specified, use it *)
-            | Some c ->
-                (try 
-		   (Ppprim.map c) sub_printer
-                 with Not_found ->
-                   (fun _ -> [< 'sTR"<printer "; 'sTR c; 'sTR" not found>" >]))
-            | None -> token_printer sub_printer
+          match externpr with (* May branch to an other printer *)
+            | Some (c,entry_prec) ->
+                (try (* Test for a primitive printer *)
+		   (Ppprim.map c) (sub_pr whatfor (Some(rule_prec,reln)))
+                 with Not_found -> token_printer (sub_pr c entry_prec))
+            | None -> token_printer (sub_pr whatfor (Some(rule_prec,reln)))
         in 
 	printer (Ast.pat_sub Ast.dummy_loc env e)
     | RO s -> [< 'sTR s >]
@@ -155,21 +152,21 @@ let print_syntax_entry sub_pr env se =
  * In the case of tactics and commands, dflt also prints 
  * global constants basenames. *)
 
-let genprint whatfor dflt inhprec ast =
-  let rec rec_pr inherited gt =
+let genprint dflt whatfor inhprec ast =
+  let rec rec_pr whatfor inherited gt =
     match find_syntax_entry whatfor gt with
       | Some(se, env) ->     
-          let rule_prec = (se.syn_id, se.syn_prec) in
-          let no_paren = tolerable_prec inherited rule_prec in
-          let printed_gt = print_syntax_entry rec_pr env se in
-          if no_paren then 
+	  let rule_prec = (se.syn_id, se.syn_prec) in
+	  let no_paren = tolerable_prec inherited rule_prec in
+	  let printed_gt = print_syntax_entry whatfor rec_pr env se in
+	  if no_paren then 
 	    printed_gt
-          else 
+	  else 
 	    [< 'sTR"(" ; printed_gt; 'sTR")" >]
       | None -> dflt gt (* No rule found *)
   in
   try 
-    rec_pr inhprec ast
+    rec_pr whatfor inhprec ast
   with
     | Failure _ -> [< 'sTR"<PP failure: "; dflt ast; 'sTR">" >]
     | Not_found -> [< 'sTR"<PP search failure: "; dflt ast; 'sTR">" >]
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index 075500c95..a7da42b9c 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -19,13 +19,12 @@ val unfreeze : frozen_t -> unit
 val find_syntax_entry :
   string -> Coqast.t -> (syntax_entry * Ast.env) option
 val add_rule : string -> syntax_entry -> unit
-val add_ppobject : (string * syntax_entry list) -> unit
+val add_ppobject : syntax_command -> unit
 
 (* Pretty-printing *)
 
 type std_printer = Coqast.t -> std_ppcmds
-type unparsing_subfunction =
-    ((string * precedence) * parenRelation) option -> std_printer
+type unparsing_subfunction = string -> tolerability option -> std_printer
 
 (* Module of primitive printers *)
 module Ppprim :
@@ -37,5 +36,5 @@ module Ppprim :
 (* Generic printing functions *) 
 val token_printer: std_printer -> std_printer
 val print_syntax_entry : 
-  unparsing_subfunction -> Ast.env -> syntax_entry -> std_ppcmds
-val genprint : string -> std_printer -> unparsing_subfunction
+  string -> unparsing_subfunction -> Ast.env -> syntax_entry -> std_ppcmds
+val genprint : std_printer -> unparsing_subfunction
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
index 5b0474156..1e2a00cce 100644
--- a/parsing/extend.ml4
+++ b/parsing/extend.ml4
@@ -8,137 +8,6 @@ open Pcoq
 open Coqast
 open Ast
 
-open Pcoq.Vernac
-
-GEXTEND Gram
-  vernac:
-    [ RIGHTA
-     [ "Drop"; "." -> <:ast< (DROP) >>
-     | "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP)>>
-     | "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
-       s = [ s = STRING -> s | s = IDENT -> s ]; "." ->
-         <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
-
-     (* TODO: deplacer vers g_vernac & Vernac.v *)
-     | "Compile";
-       verbosely =
-         [ IDENT "Verbose" -> "Verbose"
-         | -> "" ];
-       IDENT "Module";
-       only_spec =
-         [ IDENT "Specification" -> "Specification"
-         | -> "" ];
-       mname = [ s = STRING -> s | s = IDENT -> s ];
-       fname = OPT [ s = STRING -> s | s = IDENT -> s ]; "." ->
-         let fname = match fname with Some s -> s | None -> mname in
-         <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
-                   ($STR $mname) ($STR $fname))>> ]]
-  ;
-END
-
-(* These are the entries without which MakeBare cannot be compiled *)
-GEXTEND Gram
-  GLOBAL: vernac Prim.syntax_entry Prim.grammar_entry;
-
-  vernac:
-    [[ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
-
-     | "Grammar"; univ=IDENT; tl=LIST1 Prim.grammar_entry SEP "with"; "." ->
-         <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
-
-     | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
-         <:ast< (SYNTAX ($VAR whatfor) (ASTLIST ($LIST el))) >>
-     | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
-       p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
-     | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
-       p = identarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >> ]]
-  ;
-
-  (* Syntax entries for Grammar. Only grammar_entry is exported *)
-  Prim.grammar_entry:
-    [[ nont = Prim.ident; etyp = Prim.entry_type; ":=";
-       ep = entry_prec; rl = LIST0 grammar_rule SEP "|" ->
-         <:ast< (ENTRY $nont $etyp $ep ($LIST rl)) >> ]]
-  ;
-  entry_prec:
-    [[ IDENT "LEFTA" -> <:ast< {LEFTA} >>
-     | IDENT "RIGHTA" -> <:ast< {RIGHTA} >>
-     | IDENT "NONA" -> <:ast< {NONA} >>
-     | ->  <:ast< {NONE} >> ] ]
-  ;
-  grammar_rule:
-    [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
-       a = Prim.astact ->
-        <:ast< (RULE ($ID name) $a ($LIST pil)) >> ]]
-  ;
-  rule_name:
-    [[ name = IDENT -> name ]]
-  ;
-  production_item:
-    [[ s = STRING -> <:ast< ($STR $s) >>
-     | nt = non_terminal; po = OPT [ "("; p = Prim.ident; ")" -> p ] ->
-         match po with
-           | Some p -> <:ast< (NT $nt $p) >>
-           | _ -> <:ast< (NT $nt) >> ]]
-  ;
-  non_terminal:
-    [[ u = Prim.ident; ":"; nt = Prim.ident -> <:ast< (QUAL $u $nt) >>
-     | nt = Prim.ident -> <:ast< $nt >> ]]
-  ;
-
-
-  (* Syntax entries for Syntax. Only syntax_entry is exported *)
-  Prim.syntax_entry:
-    [ [ IDENT "level"; p = precedence; ":"; rl = LIST1 syntax_rule SEP "|" ->
-          <:ast< (SYNTAXENTRY $p ($LIST $rl)) >> ] ]
-  ;
-  syntax_rule:
-    [ [ nm = IDENT; "["; s = Prim.astpat; "]"; "->"; u = unparsing ->
-          <:ast< (RULE ($ID $nm) $s $u) >> ] ]
-  ;
-  precedence:
-    [ [ a = Prim.number ->  <:ast< (PREC $a 0 0) >>
-      | "["; a1 = Prim.number; a2 = Prim.number; a3 = Prim.number; "]" ->
-          <:ast< (PREC $a1 $a2 $a3) >> ] ]
-  ;
-  unparsing:
-    [ [ "["; ll = LIST0 next_hunks; "]" -> <:ast< (UNPARSING ($LIST $ll))>> ] ]
-  ;
-  next_hunks:
-    [ [ IDENT "FNL" -> <:ast< (UNP_FNL) >>
-      | IDENT "TAB" -> <:ast< (UNP_TAB) >>
-      | c = STRING -> <:ast< (RO ($STR $c)) >>
-      | "[";
-        x =
-          [ b = box; ll = LIST0 next_hunks -> <:ast<(UNP_BOX $b ($LIST $ll))>>
-          | n = Prim.number; m = Prim.number -> <:ast< (UNP_BRK $n $m) >>
-          | IDENT "TBRK";
-            n = Prim.number; m = Prim.number -> <:ast< (UNP_TBRK $n $m) >> ];
-        "]" -> x
-      | e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln -> pr ] ->
-            match oprec with
-	      | Some pr -> <:ast< (PH $e $pr) >>
-              | None -> <:ast< (PH $e {Any}) >> ]]
-  ;
-  box:
-    [ [ "<"; bk = box_kind; ">" -> bk ] ]
-  ;
-  box_kind:
-    [ [ IDENT "h"; n = Prim.number -> <:ast< (PpHB $n) >>
-      | IDENT "v"; n = Prim.number -> <:ast< (PpVB $n) >>
-      | IDENT "hv"; n = Prim.number -> <:ast< (PpHVB $n) >>
-      | IDENT "hov"; n = Prim.number -> <:ast< (PpHOVB $n) >>
-      | IDENT "t" -> <:ast< (PpTB) >> ] ]
-  ;
-  paren_reln:
-    [ [ IDENT "L" -> <:ast< {L} >>
-      | IDENT "E" -> <:ast< {E} >>
-      | pprim = STRING -> <:ast< ($STR $pprim) >> ] ]
-  ;
-END
-
-
-
 (* Converting and checking grammar command *)
 
 type nonterm =
@@ -207,12 +76,21 @@ let qualified_nterm current_univ ntrm =
       NtQual (univ, en) -> (get_univ univ, en)
     | NtShort en -> (current_univ, en)
 
+(* For compatibility *)
+let rename_command nt =
+  if String.length nt >= 7 & String.sub nt 0 7 = "command"
+  then "constr"^(String.sub nt 7 (String.length nt - 7))
+  else if nt = "lcommand" then "lconstr"
+  else if nt = "lassoc_command4" then "lassoc_constr4"
+  else nt
 
 let nterm univ ast =
+
   let nont =
     match ast with
-      | Node (_, "QUAL", [Id (_, u); Id (_, nt)]) -> NtQual (u, nt)
-      | Id (_, nt) -> NtShort nt
+      | Node (_, "QUAL", [Id (_, u); Id (_, nt)]) ->
+	  NtQual (rename_command u, rename_command nt)
+      | Id (_, nt) -> NtShort (rename_command nt)
       | _ -> invalid_arg_loc (Ast.loc ast, "Extend.nterm") 
   in
   let (u,n) = qualified_nterm univ nont in
@@ -250,7 +128,7 @@ let rec prod_item_list univ penv pil =
 
 let gram_rule univ etyp ast =
   match ast with
-    | Node (_, "RULE", (Id (_, name) :: act :: pil)) ->
+    | Node (_, "GRAMMARRULE", (Id (_, name) :: act :: pil)) ->
 	let (pilc, act_env) = prod_item_list univ [] pil in
 	let a = Ast.to_act_check_vars act_env etyp act in
         { gr_name=name; gr_production=pilc; gr_action=a }
@@ -270,9 +148,13 @@ let gram_assoc = function
   | ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.assoc")
 
 let gram_define_entry univ = function
-  | Node (_, "ENTRY", (Id (ntl, nt) :: et :: ass :: rl)) ->
+  | Node (_, "GRAMMARENTRY", (Id (ntl, nt) :: et :: ass :: rl)) ->
       let etyp = entry_type et in
       let assoc = gram_assoc ass in
+
+      (* For compatibility *)
+      let nt = rename_command nt in
+
       let _ =
         try 
 	  create_entry univ nt etyp
@@ -282,7 +164,11 @@ let gram_define_entry univ = function
       (nt, etyp, assoc, rl)
   | ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.gram_define_entry")
 
-let gram_of_ast univ astl =
+let interp_grammar_command univ astl =
+
+      (* For compatibility *)
+      let univ = rename_command univ in
+
   let u = get_univ univ in
   let entryl = List.map (gram_define_entry u) astl in
   { gc_univ = univ;
@@ -314,8 +200,10 @@ type ppbox =
   | PpVB of int
   | PpTB
 
+type tolerability = (string * precedence) * parenRelation
+
 type unparsing_hunk = 
-  | PH of Ast.pat * string option * parenRelation
+  | PH of Ast.pat * (string * tolerability option) option * parenRelation
   | RO of string
   | UNP_BOX of ppbox * unparsing_hunk list
   | UNP_BRK of int * int
@@ -340,15 +228,24 @@ let box_of_ast = function
   | Node (_, "PpTB", [])           -> PpTB
   | p -> invalid_arg_loc (Ast.loc p,"Syntaxext.box_of_ast")
 
+let prec_of_ast = function
+  | Node(_,"PREC",[Num(_,a1); Num(_,a2); Num(_,a3)]) -> (a1,a2,a3)
+  | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast")
+
+let extern_of_ast loc = function
+  | [Str(_,ppextern)] -> Some (ppextern,None)
+  | [Str(_,ppextern);p] -> Some (ppextern,Some ((ppextern,prec_of_ast p),Any))
+  |  _ -> invalid_arg_loc (loc,"Syntaxext.extern_of_ast")
+
 let rec unparsing_hunk_of_ast vars = function
-  | Node(_, "PH", [e; Str(_,pprim)]) ->
-      PH (Ast.val_of_ast vars e, Some pprim, Any)
+  | Node(_, "PH", [e; Node (loc,"EXTERN", ext_args)]) ->
+      PH (Ast.val_of_ast vars e, extern_of_ast loc ext_args, Any)
   | Node(loc, "PH", [e; Id(_,pr)]) ->
       let reln =
         (match pr with
            | "L" -> L
            | "E" -> E
-           | "Any" -> Any 
+           | "Any" -> Any
            | _ -> invalid_arg_loc (loc,"Syntaxext.paren_reln_of_ast")) in
       PH (Ast.val_of_ast vars e, None, reln)
   | Node (_, "RO", [Str(_,s)]) -> RO s
@@ -366,19 +263,18 @@ let unparsing_of_ast vars = function
       List.map (unparsing_hunk_of_ast vars) ll
   | u -> invalid_arg_loc (Ast.loc u,"Syntaxext.unp_of_ast")
 
-let prec_of_ast = function
-  | Node(_,"PREC",[Num(_,a1); Num(_,a2); Num(_,a3)]) -> (a1,a2,a3)
-  | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast")
-
-
 type syntax_entry = {
   syn_id : string;
   syn_prec: precedence;
   syn_astpat : Ast.pat;
   syn_hunks : unparsing_hunk list }
 
+type syntax_command = { 
+  sc_univ : string; 
+  sc_entries : syntax_entry list }
+
 let rule_of_ast whatfor prec = function
-  | Node(_,"RULE",[Id(_,s); spat; unp]) ->
+  | Node(_,"SYNTAXRULE",[Id(_,s); spat; unp]) ->
       let (astpat,meta_env) = Ast.to_pat [] spat in
       let hunks = unparsing_of_ast meta_env unp in
       { syn_id = s;
@@ -392,3 +288,9 @@ let level_of_ast whatfor = function
       let prec = prec_of_ast pr in
       List.map (rule_of_ast whatfor prec) rl
   | ast -> invalid_arg_loc (Ast.loc ast,"Metasyntax.level_of_ast")
+
+let interp_syntax_entry univ sel =
+  { sc_univ = univ;
+    sc_entries = List.flatten (List.map (level_of_ast univ) sel)}
+
+
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 7f9a5f569..8fe219d45 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -34,8 +34,9 @@ type grammar_command = {
   gc_univ : string; 
   gc_entries : grammar_entry list }
 
-val gram_assoc: Coqast.t -> Gramext.g_assoc option
-val gram_of_ast: string -> Coqast.t list -> grammar_command
+val gram_assoc : Coqast.t -> Gramext.g_assoc option
+
+val interp_grammar_command : string -> Coqast.t list -> grammar_command
 
 
 (*s Pretty-print. *)
@@ -50,10 +51,9 @@ type parenRelation = L | E | Any
    highest precedence), and the child's one, follow the given
    relation. *)
 
-val tolerable_prec : ((string * precedence) * parenRelation) option ->
-  (string * precedence) -> bool
+type tolerability = (string * precedence) * parenRelation
 
-val prec_of_ast : Coqast.t -> precedence
+val tolerable_prec : tolerability option -> (string * precedence) -> bool
 
 (* unparsing objects *)
 
@@ -65,7 +65,7 @@ type ppbox =
   | PpTB
 
 type unparsing_hunk = 
-  | PH of Ast.pat * string option * parenRelation
+  | PH of Ast.pat * (string * tolerability option) option * parenRelation
   | RO of string
   | UNP_BOX of ppbox * unparsing_hunk list
   | UNP_BRK of int * int
@@ -83,8 +83,10 @@ type syntax_entry = {
   syn_astpat : Ast.pat;
   syn_hunks : unparsing_hunk list }
 
-val rule_of_ast : string -> precedence -> Coqast.t -> syntax_entry
+type syntax_command = { 
+  sc_univ : string; 
+  sc_entries : syntax_entry list }
 
-val level_of_ast : string -> Coqast.t -> syntax_entry list
+val interp_syntax_entry : string -> Coqast.t list -> syntax_command
 
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 873d52cbb..6da37473f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -71,7 +71,7 @@ module Gram =
   end
 
 
-(* This extension command is used by the Grammar command *)
+(* This extension command is used by the Grammar constr *)
 
 let grammar_extend te pos rls =
   camlp4_state := ByGrammar (te,pos,rls) :: !camlp4_state;
@@ -205,60 +205,54 @@ let force_entry_type (u, utab) s etyp =
 
 (* Grammar entries *)
 
-module Command =
+module Constr =
   struct
-    let ucommand = snd (get_univ "command")
+    let uconstr = snd (get_univ "constr")
     let gec s =
-      let e = Gram.Entry.create ("Command." ^ s) in
-      Hashtbl.add ucommand s (Ast e); e
+      let e = Gram.Entry.create ("Constr." ^ s) in
+      Hashtbl.add uconstr s (Ast e); e
 	
     let gec_list s =
-      let e = Gram.Entry.create ("Command." ^ s) in
-      Hashtbl.add ucommand s (ListAst e); e
+      let e = Gram.Entry.create ("Constr." ^ s) in
+      Hashtbl.add uconstr s (ListAst e); e
+
+    let constr = gec "constr"
+    let constr0 = gec "constr0"
+    let constr1 = gec "constr1"
+    let constr2 = gec "constr2"
+    let constr3 = gec "constr3"
+    let lassoc_constr4 = gec "lassoc_constr4"
+    let constr5 = gec "constr5"
+    let constr6 = gec "constr6"
+    let constr7 = gec "constr7"
+    let constr8 = gec "constr8"
+    let constr9 = gec "constr9"
+    let constr91 = gec "constr91"
+    let constr10 = gec "constr10"
+    let constr_eoi = eoi_entry constr
+    let lconstr = gec "lconstr"
+    let ident = gec "ident"
+    let ne_ident_comma_list = gec_list "ne_ident_comma_list"
+    let ne_constr_list = gec_list "ne_constr_list"
 
-    let abstraction_tail = gec "abstraction_tail"
+    let pattern = Gram.Entry.create "Constr.pattern"
+
+(*
     let binder = gec "binder"
+
+    let abstraction_tail = gec "abstraction_tail"
     let cofixbinder = gec "cofixbinder"
     let cofixbinders = gec_list "cofixbinders"
-    let command = gec "command"
-    let command0 = gec "command0"
-    let command1 = gec "command1"
-    let command10 = gec "command10"
-    let command2 = gec "command2"
-    let command3 = gec "command3"
-    let command5 = gec "command5"
-    let command6 = gec "command6"
-    let command7 = gec "command7"
-    let command8 = gec "command8"
-    let command9 = gec "command9"
-    let command91 = gec "command91"
-    let command_eoi = eoi_entry command
-    let equation = gec "equation"
     let fixbinder = gec "fixbinder"
     let fixbinders = gec_list "fixbinders"
-    let ident = gec "ident"
-    let lassoc_command4 = gec "lassoc_command4"
-    let lcommand = gec "lcommand"
-    let lsimple_pattern = Gram.Entry.create "Command.lsimple_pattern"
+
     let ne_binder_list = gec_list "ne_binder_list"
-    let ne_command91_list = gec_list "ne_command91_list"
-    let ne_command9_list = gec_list "ne_command9_list"
-    let ne_command_list = gec_list "ne_command_list"
-    let ne_eqn_list = gec_list "ne_eqn_list"
-    let ne_ident_comma_list = gec_list "ne_ident_comma_list"
-    let ne_pattern_list = Gram.Entry.create "Command.ne_pattern_list"
-    let pattern = Gram.Entry.create "Command.pattern"
-    let pattern_list = Gram.Entry.create "Command.pattern_list"
-    let product_tail = gec "product_tail"
-    let raw_command = gec "raw_command"
-    let simple_pattern = Gram.Entry.create "Command.simple_pattern"
-    let simple_pattern2 = Gram.Entry.create "Command.simple_pattern2"
-    let simple_pattern_list =
-	 Gram.Entry.create "Command.simple_pattern_list"
-    let type_option = gec "type_option"
-    let weak_binder = gec "weak_binder"
-    let ne_weak_binder_list = gec_list "ne_weak_binder"
-    let ucommand = snd (get_univ "command")
+
+    let ne_pattern_list = Gram.Entry.create "Constr.ne_pattern_list"
+    let pattern_list = Gram.Entry.create "Constr.pattern_list"
+    let simple_pattern = Gram.Entry.create "Constr.simple_pattern"
+*)
+    let uconstr = snd (get_univ "constr")
   end
 
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index de8c7128e..8bc7642e3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -56,49 +56,44 @@ val main_entry : Coqast.t option Gram.Entry.e
 
 (* Initial state of the grammar *)
 
-module Command :
+module Constr :
   sig
-    val abstraction_tail : Coqast.t Gram.Entry.e
+    val constr : Coqast.t Gram.Entry.e
+    val constr0 : Coqast.t Gram.Entry.e
+    val constr1 : Coqast.t Gram.Entry.e
+    val constr2 : Coqast.t Gram.Entry.e
+    val constr3 : Coqast.t Gram.Entry.e
+    val lassoc_constr4 : Coqast.t Gram.Entry.e
+    val constr5 : Coqast.t Gram.Entry.e
+    val constr6 : Coqast.t Gram.Entry.e
+    val constr7 : Coqast.t Gram.Entry.e
+    val constr8 : Coqast.t Gram.Entry.e
+    val constr9 : Coqast.t Gram.Entry.e
+    val constr91 : Coqast.t Gram.Entry.e
+    val constr10 : Coqast.t Gram.Entry.e
+    val constr_eoi : Coqast.t Gram.Entry.e
+    val lconstr : Coqast.t Gram.Entry.e
+    val ident : Coqast.t Gram.Entry.e
+    val ne_ident_comma_list : Coqast.t list Gram.Entry.e
+    val ne_constr_list : Coqast.t list Gram.Entry.e
+
+    val pattern : Coqast.t Gram.Entry.e
+
+(*
     val binder : Coqast.t Gram.Entry.e
+
+    val abstraction_tail : Coqast.t Gram.Entry.e
     val cofixbinder : Coqast.t Gram.Entry.e
     val cofixbinders : Coqast.t list Gram.Entry.e
-    val command : Coqast.t Gram.Entry.e
-    val command0 : Coqast.t Gram.Entry.e
-    val command1 : Coqast.t Gram.Entry.e
-    val command10 : Coqast.t Gram.Entry.e
-    val command2 : Coqast.t Gram.Entry.e
-    val command3 : Coqast.t Gram.Entry.e
-    val command5 : Coqast.t Gram.Entry.e
-    val command6 : Coqast.t Gram.Entry.e
-    val command7 : Coqast.t Gram.Entry.e
-    val command8 : Coqast.t Gram.Entry.e
-    val command9 : Coqast.t Gram.Entry.e
-    val command91 : Coqast.t Gram.Entry.e
-    val command_eoi : Coqast.t Gram.Entry.e
-    val equation : Coqast.t Gram.Entry.e
     val fixbinder : Coqast.t Gram.Entry.e
     val fixbinders : Coqast.t list Gram.Entry.e
-    val ident : Coqast.t Gram.Entry.e
-    val lassoc_command4 : Coqast.t Gram.Entry.e
-    val lcommand : Coqast.t Gram.Entry.e
-    val lsimple_pattern : Coqast.t Gram.Entry.e
+
     val ne_binder_list : Coqast.t list Gram.Entry.e
-    val ne_command91_list : Coqast.t list Gram.Entry.e
-    val ne_command9_list : Coqast.t list Gram.Entry.e
-    val ne_command_list : Coqast.t list Gram.Entry.e
-    val ne_eqn_list : Coqast.t list Gram.Entry.e
-    val ne_ident_comma_list : Coqast.t list Gram.Entry.e
+
     val ne_pattern_list : Coqast.t list Gram.Entry.e
-    val pattern : Coqast.t Gram.Entry.e
     val pattern_list : Coqast.t list Gram.Entry.e
-    val product_tail : Coqast.t Gram.Entry.e
-    val raw_command : Coqast.t Gram.Entry.e
     val simple_pattern : Coqast.t Gram.Entry.e
-    val simple_pattern2 : Coqast.t Gram.Entry.e
-    val simple_pattern_list : Coqast.t list Gram.Entry.e
-    val type_option : Coqast.t Gram.Entry.e
-    val weak_binder : Coqast.t Gram.Entry.e
-    val ne_weak_binder_list : Coqast.t list Gram.Entry.e
+*)
   end
 
 module Tactic :
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 8147fd2b8..3e522f95c 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -43,8 +43,8 @@ let print_closed_sections = ref false
 
 let print_typed_value_in_env env (trm,typ) =
   let sign = Environ.var_context env in
-  [< term0 (gLOB sign) trm ; 'fNL ;
-     'sTR "     : "; term0 (gLOB sign) typ ; 'fNL >]
+  [< prterm_env (gLOB sign) trm ; 'fNL ;
+     'sTR "     : "; prterm_env (gLOB sign) typ ; 'fNL >]
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
 			  		  
@@ -77,7 +77,7 @@ let print_var name typ =
   [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
 
 let print_env pk = 
-  let pterminenv = if pk = FW then fterm0 else term0 in
+  let pterminenv = if pk = FW then fprterm_env else prterm_env in
   let pr_binder env (na,c) =
     match na with
       | Name id as name ->
@@ -99,7 +99,7 @@ let assumptions_for_print lna =
 
 let print_constructors_with_sep pk fsep mip = 
   let pterm,pterminenv =
-    if pk = FW then (fprterm,fterm0) else (prterm,term0) in
+    if pk = FW then (fprterm,fprterm_env) else (prterm,prterm_env) in
   let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = Array.to_list 
@@ -131,7 +131,7 @@ let implicit_args_msg sp mipv =
 let print_mutual sp mib = 
   let pk = kind_of_path sp in
   let pterm,pterminenv =
-    if pk = FW then (fprterm,fterm0) else (prterm,term0) in
+    if pk = FW then (fprterm,fprterm_env) else (prterm,prterm_env) in
   let env = Global.env () in
   let evd = Evd.empty in
   let {mind_packets=mipv; mind_nparams=nparams} = mib in 
@@ -395,7 +395,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
 
 let print_crible name =
   crible (fun str ass_name constr -> 
-            let pc = term0 ass_name constr in
+            let pc = prterm_env ass_name constr in
             mSG[<'sTR str; 'sTR":"; pc; 'fNL >]) name
 
 let read_sec_context sec =
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 392078611..c93fdbb48 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -10,56 +10,25 @@ open Environ
 open Global
 open Declare
 open Coqast
+open Termast
 
-let print_arguments = ref false
-let print_casts = ref false
-let print_emacs = ref false
+let emacs_str s = if !Options.print_emacs then s else "" 
 
-let emacs_str s =
-  if !print_emacs then s else "" 
+let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >];;
 
+(*
 let section_path sl s =
   let sl = List.rev sl in
   make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)
 
-let with_implicits f x =
-  let oimpl = !Termast.print_implicits in
-  Termast.print_implicits := true; 
-  try
-    let r = f x in
-    Termast.print_implicits := oimpl;
-    r
-  with e -> 
-    Termast.print_implicits := oimpl; raise e
-
-let pr_qualified sp id = 
-  if Nametab.sp_of_id (kind_of_path sp) id = sp then 
-    [< 'sTR(string_of_id id) >]
-  else 
-    [< 'sTR(string_of_path sp) >]
-
-let pr_constant (sp,_) = pr_qualified sp (basename sp)
-
-let pr_existential (ev,_) = [< 'sTR ("?" ^ string_of_int ev) >]
-
-let pr_inductive (sp,tyi as ind_sp,_) =
-  let id = id_of_global (MutInd ind_sp) in
-  pr_qualified sp id
-
-let pr_constructor ((sp,tyi),i as cstr_sp,_) =
-  let id = id_of_global (MutConstruct cstr_sp) in
-  pr_qualified sp id
-
-(*
 let pr_global k oper =
   let id = id_of_global oper in
   [< 'sTR (string_of_id id) >]
 *)
 
-let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >]
-
 let globpr k gt = match gt with
   | Nvar(_,s) -> [< 'sTR s >]
+(*
   | Node(_,"EVAR", (Num (_,ev))::_) ->
       if !print_arguments then dfltpr gt
       else pr_existential (ev,[])
@@ -72,29 +41,10 @@ let globpr k gt = match gt with
   | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) ->
       if !print_arguments then (dfltpr gt)
       else pr_constructor (((section_path sl s,tyi),i),[])
+*)
   | gt -> dfltpr gt
 
-let apply_prec = Some (("Term",(9,0,0)),Extend.L)
-let apply_tacprec = Some (("Tactic",(9,0,0)),Extend.L)
-
-let rec gencompr k gt =
-  let uni = match k with
-    | CCI | FW -> "constr"
-    | _ -> "<undefined>" 
-  in
-  let rec gpr gt =
-    Esyntax.genprint uni
-      (function
-         | Node(_,"PPUNI$COMMAND",[Str(_,"CCI");c]) -> gencompr CCI c
-         | Node(_,"PPUNI$COMMAND",[c]) -> gencompr CCI c
-         | Node(_,"PPUNI$COMMAND",[Str(_,"FW");c]) -> gencompr FW c
-         | gt -> globpr k gt)
-      apply_prec
-      gt
-  in 
-  gpr gt
-
-let print_if_exception = function
+let wrap_exception = function
     Anomaly (s1,s2) ->
       warning ("Anomaly ("^s1^")");pP s2;
       [< 'sTR"<PP error: non-printable term>" >]
@@ -102,75 +52,75 @@ let print_if_exception = function
       [< 'sTR"<PP error: non-printable term>" >]
   | s -> raise s
 
+(* These are the names of the universes where the pp rules for constr and
+   tactic are put (must be consistent with files PPConstr.v and PPTactic.v *)
+
+let constr_syntax_universe = "constr"
+let tactic_syntax_universe = "tactic"
+
+(* This is starting precedence for printing constructions or tactics *)
+(* Level 9 means no parentheses except for applicative terms (at level 10) *)
+let constr_initial_prec = Some ((constr_syntax_universe,(9,0,0)),Extend.L)
+let tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Extend.L)
+
+let gencompr k gt =
+  let uni = match k with
+    | CCI | FW -> constr_syntax_universe
+    | _ -> anomaly "gencompr: not a construction"
+	(* WAS "<undefined>" *)
+  in Esyntax.genprint (globpr k) uni constr_initial_prec gt
+
 (* [at_top] means ids of env must be avoided in bound variables *)
 let gentermpr_core at_top k env t =
   let uenv = unitize_env env in
-  try 
-    let ogt = 
-      if !print_casts then 
-	Termast.bdize at_top uenv t
-      else 
-	Termast.bdize_no_casts at_top uenv t
-    in 
-    gencompr k ogt
-  with s -> print_if_exception s
+  try gencompr k (Termast.bdize at_top uenv t)
+  with s -> wrap_exception s
 
-let term0_at_top a = gentermpr_core true CCI a
-let gentermpr a = gentermpr_core false a
+let gentermpr k = gentermpr_core false k
 
-let term0 a = gentermpr CCI a
-let prterm = term0 (gLOB nil_sign)
-let fterm0 a = gentermpr FW a
-let fprterm = fterm0 (gLOB nil_sign)
+let prterm_env_at_top a = gentermpr_core true CCI a
+let prterm_env a = gentermpr CCI a
+let prterm = prterm_env (gLOB nil_sign)
 
-let prtype_env env typ =
-  if !print_casts then 
-    term0 env (mkCast typ.body (mkSort typ.typ))
-  else 
-    prterm typ.body
+let fprterm_env a = gentermpr FW a
+let fprterm = fprterm_env (gLOB nil_sign)
 
+let prtype_env env typ = prterm_env env (mkCast typ.body (mkSort typ.typ))
 let prtype = prtype_env (gLOB nil_sign)
 
-let fprtype_env env typ =
-  if !print_casts then 
-    fterm0 env (mkCast typ.body (mkSort typ.typ))
-  else 
-    fterm0 env typ.body
-
+let fprtype_env env typ = fprterm_env env (mkCast typ.body (mkSort typ.typ))
 let fprtype = fprtype_env (gLOB nil_sign)
 
+let pr_constant cst = gencompr CCI (ast_of_constant cst)
+let pr_existential ev = gencompr CCI (ast_of_existential ev)
+let pr_inductive ind = gencompr CCI (ast_of_inductive ind)
+let pr_constructor cstr = gencompr CCI (ast_of_constructor cstr)
+
+(* For compatibility *)
+let term0 = prterm_env
+let fterm0 = fprterm_env
+
 let genpatternpr k t =
-  try 
-    gencompr k (Termast.ast_of_pattern t)
-  with s -> print_if_exception s
+  try gencompr k (Termast.ast_of_pattern t)
+  with s -> wrap_exception s
 
 let prpattern = genpatternpr CCI
 
 let genrawtermpr k env t =
-  try 
-    gencompr k (Termast.ast_of_rawconstr t)
-  with s -> print_if_exception s
+  try gencompr k (Termast.ast_of_rawconstr t)
+  with s -> wrap_exception s
 
 let prrawterm = genrawtermpr CCI (gLOB nil_sign)
 
-let gentacpr gt =
-  let rec gpr gt =
-    Esyntax.genprint "tactic"
-      (function 
-         | Nvar(_,s) -> [< 'sTR s >]
-         | Node(_,"PPUNI$COMMAND",[Str(_,"CCI");c]) -> gencompr CCI c
-         | Node(_,"PPUNI$COMMAND",[c]) -> gencompr CCI c
-         | Node(_,"PPUNI$COMMAND",[Str(_,"FW");c]) -> gencompr FW c
-         | gt -> default_tacpr gt)
-      apply_tacprec
-      gt
-  and default_tacpr = function
+let rec gentacpr gt =
+  Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
+
+and default_tacpr = function
+    | Nvar(_,s) -> [< 'sTR s >]
     | Node(_,s,[]) -> [< 'sTR s >]
     | Node(_,s,ta) ->
-	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gpr ta) >]
+	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
     | gt -> dfltpr gt
-  in 
-  gpr gt
 
 let print_decl k sign (s,typ) =
   let ptyp = gentermpr k (gLOB sign) typ.body in
@@ -262,5 +212,3 @@ let pr_env_limit n env =
 let pr_env_opt env = match Options.print_hyps_limit () with 
   | None -> hV 0 (pr_env CCI env)
   | Some n -> hV 0 (pr_env_limit n env)
-
-let emacs_str s = if !Options.print_emacs then s else "" 
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 0f704c552..1b5517890 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -8,21 +8,20 @@ open Term
 open Sign
 (*i*)
 
+(* These are the entry points for printing terms, context, tac, ... *)
 val gencompr  : path_kind -> Coqast.t -> std_ppcmds
 val gentermpr : path_kind -> 'a assumptions -> constr -> std_ppcmds
 val gentacpr  : Coqast.t -> std_ppcmds
 
+val prterm_env      : 'a assumptions -> constr -> std_ppcmds
+val prterm_env_at_top : 'a assumptions -> constr -> std_ppcmds
 val prterm          : constr -> std_ppcmds
 val prtype_env      : 'a assumptions -> typed_type -> std_ppcmds
 val prtype          : typed_type -> std_ppcmds
+val fprterm_env     : 'a assumptions -> constr -> std_ppcmds
 val fprterm         : constr -> std_ppcmds
 val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
 val fprtype         : typed_type -> std_ppcmds
-val fterm0          : 'a assumptions -> constr -> std_ppcmds
-val term0           : 'a assumptions -> constr -> std_ppcmds
-val term0_at_top    : 'a assumptions -> constr -> std_ppcmds
-
-val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
 
 val prrawterm       : Rawterm.rawconstr -> std_ppcmds
 val prpattern       : Rawterm.pattern -> std_ppcmds
@@ -32,12 +31,14 @@ val pr_existential  : existential -> std_ppcmds
 val pr_constructor  : constructor -> std_ppcmds
 val pr_inductive    : inductive -> std_ppcmds
 
+val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
+
 val pr_sign         : var_context -> std_ppcmds
 val pr_env_opt      : context -> std_ppcmds
 
-val print_arguments : bool ref
-val print_casts     : bool ref
-val print_emacs     : bool ref
-val with_implicits  : ('a -> 'b) -> 'a -> 'b
-
 val emacs_str       : string -> string
+
+(* For compatibility *)
+val fterm0          : 'a assumptions -> constr -> std_ppcmds
+val term0           : 'a assumptions -> constr -> std_ppcmds
+
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 5a1327430..ae8d8bfd3 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -97,9 +97,9 @@ let f e =
   Quotation.ExAst (ee, ep)
 
 let _ = 
-  Quotation.add "command" (f Pcoq.Command.command_eoi);
+  Quotation.add "constr" (f Pcoq.Constr.constr_eoi);
   Quotation.add "tactic" (f Pcoq.Tactic.tactic_eoi);
   Quotation.add "vernac" (f Pcoq.Vernac.vernac_eoi);
   Quotation.add "ast" (f Pcoq.Prim.ast_eoi);
-  Quotation.default := "command"
+  Quotation.default := "constr"
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index b33ea0053..6b134ed34 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -15,17 +15,42 @@ open Coqast
 open Ast
 open Rawterm
 
-(* In this file, we translate constr to ast, in order to print constr *)
+(* In this file, we translate rawconstr to ast, in order to print constr *)
+
+(**********************************************************************)
+(* Parametrization                                                    *)
+
+(* This governs printing of local context of references *)
+let print_arguments = ref false
+
+(* This forces printing of cast nodes *)
+let print_casts = ref false
+
+(* This governs printing of implicit arguments.  When
+   [print_implicits] is on then [print_implicits_explicit_args] tells
+   how jimplicit args are printed. If on, implicit args are printed
+   prefixed by "!" otherwise the function and not the arguments is
+   prefixed by "!" *)
+let print_implicits = ref false
+let print_implicits_explicit_args = ref false
+
+(* This forces printing of coercions *)
+let print_coercions = ref false
+
+let with_option o f x =
+  let old = !o in o:=true;
+  try let r = f x in o := old; r
+  with e -> o := old; raise e
+
+let with_arguments f = with_option print_arguments f
+let with_casts f = with_option print_casts f
+let with_implicits f = with_option print_implicits f
+let with_coercions f = with_option print_coercions f
 
 (**********************************************************************)
 (* conversion of references                                           *)
 
-let ids_of_var cl =
-  List.map
-    (function 
-       | RRef (_,RVar id) -> id
-       | _-> anomaly "ids_of_var")
-    (Array.to_list cl)
+let ids_of_ctxt = array_map_to_list (function VAR id -> id | _ -> assert false)
 
 let ast_of_ident id = nvar (string_of_id id)
 
@@ -37,26 +62,50 @@ let stringopt_of_name = function
   | Name id -> Some (string_of_id id)
   | Anonymous -> None
 
-let ast_of_constructor (((sp,tyi),n),ids) =
-  ope("MUTCONSTRUCT",
-      (path_section dummy_loc sp)::(num tyi)::(num n)
-      ::(List.map ast_of_ident ids))
+let ast_of_qualified sp id =
+  if Nametab.sp_of_id (kind_of_path sp) id = sp then nvar (string_of_id id)
+  else nvar (string_of_path sp)
+
+let ast_of_constant_ref (sp,ids) =
+  if !print_arguments then
+    ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident ids))
+  else ast_of_qualified sp (basename sp)
+
+let ast_of_constant (ev,ids) = ast_of_constant_ref (ev,ids_of_ctxt ids)
+
+let ast_of_existential_ref (ev,ids) =
+  if !print_arguments then
+      ope("EVAR", (num ev)::(List.map ast_of_ident ids))
+  else nvar ("?" ^ string_of_int ev)
+
+let ast_of_existential (ev,ids) = ast_of_existential_ref (ev,ids_of_ctxt ids)
+
+let ast_of_constructor_ref (((sp,tyi),n) as cstr_sp,ids) =
+  if !print_arguments then
+    ope("MUTCONSTRUCT",
+	(path_section dummy_loc sp)::(num tyi)::(num n)
+	::(List.map ast_of_ident ids))
+  else ast_of_qualified sp (Global.id_of_global (MutConstruct cstr_sp))
+
+let ast_of_constructor (ev,ids) = ast_of_constructor_ref (ev,ids_of_ctxt ids)
+
+let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) =
+  if !print_arguments then
+    ope("MUTIND",
+	(path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids))
+  else ast_of_qualified sp (Global.id_of_global (MutInd ind_sp))
+
+let ast_of_inductive (ev,ids) = ast_of_inductive_ref (ev,ids_of_ctxt ids)
 
-let ast_of_mutind ((sp,tyi),ids) =
-  ope("MUTIND",
-      (path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids))
-    
 let ast_of_ref = function
-  | RConst (sp,idl) ->
-      ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident idl))
+  | RConst (sp,ids) -> ast_of_constant_ref (sp,ids)
   | RAbst (sp) ->
       ope("ABST", (path_section dummy_loc sp)
 	    ::(List.map ast_of_ident (* on triche *) []))
-  | RInd (ind,idl) -> ast_of_mutind(ind,idl)
-  | RConstruct (cstr,idl) -> ast_of_constructor (cstr,idl)
+  | RInd (ind,ids) -> ast_of_inductive_ref (ind,ids)
+  | RConstruct (cstr,ids) -> ast_of_constructor_ref (cstr,ids)
   | RVar id -> nvar (string_of_id id)
-  | REVar (ev,idl) ->
-      ope("EVAR", (num ev)::(List.map ast_of_ident idl))
+  | REVar (ev,ids) -> ast_of_existential_ref (ev,ids)
   | RMeta n -> ope("META",[num n])
 
 (**********************************************************************)
@@ -69,11 +118,181 @@ let rec ast_of_pattern = function   (* loc is thrown away for printing *)
       ope("PATTAS",
 	  [nvar (string_of_id id);
 	   ope("PATTCONSTRUCT",
-	       (ast_of_constructor cstr)::List.map ast_of_pattern args)])
+	       (ast_of_constructor_ref cstr)::List.map ast_of_pattern args)])
   | PatCstr(loc,cstr,args,Anonymous) ->
       ope("PATTCONSTRUCT",
-	  (ast_of_constructor cstr)::List.map ast_of_pattern args)
+	  (ast_of_constructor_ref cstr)::List.map ast_of_pattern args)
 	
+let ast_dependent na aty =
+  match na with
+    | Name id -> occur_var_ast (string_of_id id) aty
+    | Anonymous -> false
+
+(* Implicit args indexes are in ascending order *)
+let explicitize =
+  let rec exprec n lastimplargs impl = function
+    | a::args ->
+	(match impl with
+	   | i::l when i=n ->
+	       exprec (n+1) (ope("EXPL", [num i; a])::lastimplargs) l args
+	   | _ ->
+	       let tail = a::(exprec (n+1) [] impl args) in
+	       if (!print_implicits & !print_implicits_explicit_args) then
+		 List.rev_append lastimplargs tail
+	       else tail)
+    (* Tail impl args are always printed even if implicit printing is off *)
+    | [] -> List.rev lastimplargs
+  in exprec 0 []
+
+let implicit_of_ref = function
+  | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
+  | RInd (indid,_) -> inductive_implicits_list indid
+  | RConst (sp,_) -> constant_implicits_list sp
+  | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
+  | _ -> []
+
+let rec skip_coercion (f,args as app) =
+  if !print_coercions then app
+  else
+    try
+      match f with
+	| RRef (_,r) ->
+	    let n = Classops.coercion_params r in
+	    if n >= List.length args then app
+	    else (* We skip a coercion *)
+	      let _,fargs = list_chop n args in
+	      skip_coercion (List.hd fargs,List.tl fargs)
+	| _ -> app
+    with Not_found -> app
+
+let ast_of_app impl f args =
+  if !print_implicits & not !print_implicits_explicit_args then 
+    ope("APPLISTEXPL", f::args)
+  else
+    ope("APPLIST", f::(explicitize impl args))
+(*
+    let largs = List.length args in
+    let impl = List.rev (List.filter (fun i -> i <= largs) impl) in
+    let impl1,impl2 = div_implicits largs impl in
+    let al1 = Array.of_list args in
+    List.iter
+      (fun i -> al1.(i) <-
+         ope("EXPL", [str "EX"; num i; al1.(i)]))
+      impl2;
+    List.iter
+      (fun i -> al1.(i) <-
+         ope("EXPL",[num i; al1.(i)]))
+      impl1;
+    (* On laisse les implicites, à charge du PP de ne pas les imprimer *)
+    ope("APPLISTEXPL",f::(Array.to_list al1))
+*)
+
+let rec ast_of_raw = function
+  | RRef (_,ref) -> ast_of_ref ref
+  | RApp (_,f,args) ->
+      let (f,args) = skip_coercion (f,args) in
+      let astf = ast_of_raw f in
+      let astargs = List.map ast_of_raw args in
+      (match f with 
+	 | RRef (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs
+	 | _           -> ast_of_app [] astf astargs)
+  | RBinder (_,BProd,Anonymous,t,c) ->
+      (* Anonymous product are never factorized *)
+      ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
+  | RBinder (_,bk,na,t,c) ->
+      let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
+      let tag = match bk with
+	  (* LAMBDA et LAMBDALIST se comportent pareil *)
+	| BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST"
+	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
+	  (* non dépendant, pour isoler l'implication; peut-être un *)
+	  (* constructeur ARROW serait-il plus justifié ? *) 
+	| BProd -> if n=1 then "PROD" else "PRODLIST" 
+      in
+      ope(tag,[ast_of_raw t;a])
+
+  | RCases (_,printinfo,typopt,tml,eqns) ->
+      let pred = ast_of_rawopt typopt in
+      let tag = match printinfo with
+	| PrintIf -> "FORCEIF"
+	| PrintLet -> "FORCELET"
+	| PrintCases -> "CASES" 
+      in
+      let asttomatch = ope("TOMATCH", List.map ast_of_raw tml) in
+      let asteqns = List.map ast_of_eqn eqns in 
+      ope(tag,pred::asttomatch::asteqns)
+	
+  | ROldCase (_,isrec,typopt,tm,bv) ->
+      warning "Old Case syntax";
+      ope("MUTCASE",(ast_of_rawopt typopt)
+	    ::(ast_of_raw tm)
+	    ::(Array.to_list (Array.map ast_of_raw bv)))
+  | RRec (_,fk,idv,tyv,bv) ->
+      let alfi = Array.map ast_of_ident idv in
+      (match fk with
+	 | RFix (nv,n) ->
+             let rec split_lambda binds = function
+	       | (0, t) -> (binds,ast_of_raw t)
+	       | (n, RBinder(_,BLambda,na,t,b)) ->
+		   let bind = ope("BINDER",[ast_of_raw t;ast_of_name na]) in
+		   split_lambda (bind::binds) (n-1,b)
+	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
+	     let rec split_product = function
+	       | (0, t) -> ast_of_raw t
+	       | (n, RBinder(_,BProd,na,t,b)) -> split_product (n-1,b)
+	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
+	     let listdecl = 
+	       Array.mapi
+		 (fun i fi ->
+		    let (lparams,astdef) = split_lambda [] (nv.(i)+1,bv.(i)) in
+		    let asttyp = split_product (nv.(i)+1,tyv.(i)) in
+		    ope("FDECL",
+		       	[fi; ope ("BINDERS",List.rev lparams); 
+			 asttyp; astdef]))
+		 alfi
+	     in 
+	     ope("FIX", alfi.(n)::(Array.to_list listdecl))
+	 | RCofix n -> 
+	     let listdecl =
+               Array.mapi 
+		 (fun i fi ->
+		    ope("CFDECL",[fi; ast_of_raw tyv.(i); ast_of_raw bv.(i)]))
+		 alfi
+	     in 
+	     ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
+
+  | RSort (_,s) ->
+      (match s with
+	 | RProp Null -> ope("PROP",[])
+	 | RProp Pos -> ope("SET",[])
+	 | RType -> ope("TYPE",[]))
+  | RHole _ -> ope("ISEVAR",[])
+  | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
+	
+and ast_of_eqn (ids,pl,c) =
+  ope("EQN", (ast_of_raw c)::(List.map ast_of_pattern pl))
+
+and ast_of_rawopt = function
+  | None -> (str "SYNTH")
+  | Some p -> ast_of_raw p
+
+and factorize_binder n oper na aty c =
+  let (p,body) = match c with
+    | RBinder(_,oper',na',ty',c')
+	when (oper = oper') & (aty = ast_of_raw ty')
+	  & not (ast_dependent na aty) (* To avoid na in ty' escapes scope *)
+	  & not (na' = Anonymous & oper = BProd)
+	  -> factorize_binder (n+1) oper na' aty c'
+    | _ -> (n,ast_of_raw c)
+  in
+  (p,slam(stringopt_of_name na, body))
+
+let ast_of_rawconstr = ast_of_raw
+
+(*****************************************************************)
+(* TO EJECT ... REPRIS DANS detyping *)
+
+
 (* Nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
@@ -208,127 +427,6 @@ let sp_of_spi ((sp,_) as spi) =
   let (pa,_,k) = repr_path sp in 
   make_path pa (mip.mind_typename) k
 
-
-(* Parameterization of the translation from constr to ast      *)
-
-(* Tables for Cases printing under a "if" form, a "let" form,  *)
-
-let isomorphic_to_bool lc =
-  let lcparams = Array.map get_params lc in
-  Array.length lcparams = 2 & lcparams.(0) = [] & lcparams.(1) = []
-
-let isomorphic_to_tuple lc = (Array.length lc = 1)
-
-module PrintingCasesMake =
-  functor (Test : sig 
-     val test : constr array -> bool
-     val error_message : string
-     val member_message : identifier -> bool -> string
-     val field : string
-     val title : string
-  end) ->
-  struct
-    type t = section_path * int
-    let encode = indsp_of_id
-    let check indsp =
-      if not (Test.test (lc_of_lmis (mind_specif_of_mind_light indsp))) then 
-	errorlabstrm "check_encode" [< 'sTR Test.error_message >]
-    let decode = sp_of_spi
-    let key = Goptions.SecondaryTable ("Printing",Test.field)
-    let title = Test.title
-    let member_message = Test.member_message
-    let synchronous = true
-  end
-
-module PrintingCasesIf =
-  PrintingCasesMake (struct 
-    let test = isomorphic_to_bool
-    let error_message = "This type cannot be seen as a boolean type"
-    let field = "If"
-    let title = "Types leading to pretty-printing of Cases using a `if' form: "
-    let member_message id = function
-      | true  -> 
-          "Cases on elements of " ^ (string_of_id id)
-          ^ " are printed using a `if' form"
-      | false -> 
-          "Cases on elements of " ^ (string_of_id id)
-          ^ " are not printed using `if' form"
-  end)
-
-module PrintingCasesLet =
-  PrintingCasesMake (struct 
-    let test = isomorphic_to_tuple
-    let error_message = "This type cannot be seen as a tuple type"
-    let field = "Let"
-    let title = 
-      "Types leading to a pretty-printing of Cases using a `let' form:"
-    let member_message id = function
-      | true  -> 
-          "Cases on elements of " ^ (string_of_id id)
-          ^ " are printed using a `let' form"
-      | false -> 
-          "Cases on elements of " ^ (string_of_id id)
-          ^ " are not printed using a `let' form"
-  end)
-
-module PrintingIf  = Goptions.MakeTable(PrintingCasesIf)
-module PrintingLet = Goptions.MakeTable(PrintingCasesLet)
-
-(* Options for printing or not wildcard and synthetisable types *)
-
-open Goptions
-
-let wildcard_value = ref true
-let force_wildcard () = !wildcard_value
-
-let _ =                           
-  declare_async_bool_option 
-    { optasyncname  = "the forced wildcard option";
-      optasynckey   = SecondaryTable ("Printing","Wildcard");
-      optasyncread  = force_wildcard;
-      optasyncwrite = (fun v -> wildcard_value := v) }
-
-let synth_type_value = ref true
-let synthetize_type () = !synth_type_value
-
-let _ = 
-  declare_async_bool_option 
-    { optasyncname = "the synthesisablity";
-      optasynckey   = SecondaryTable ("Printing","Synth");
-      optasyncread = synthetize_type;
-      optasyncwrite = (fun v -> synth_type_value := v) }
-
-(* Printing of implicit *)
-
-let print_implicits = ref false
-
-
-(**************************************************)
-(* The main translation function is bdize_depcast *)
-
-(* pour les implicites *)
-
-(* l est ordonne'ee (croissant), ne garder que les elements <= n *)
-let filter_until n l =
-  let rec aux = function
-    | [] -> []
-    | i::l -> if i > n then [] else i::(aux l)
-  in 
-  aux l
-
-(* l est ordonne'e (de'croissant), n>=max(l), diviser l en deux listes,
-   la 2eme est la plus longue se'quence commencant par n,
-   la 1ere contient les autres elements *)
-
-let rec div_implicits n = 
-  function 
-    | [] -> [],[]
-    | i::l -> 
-	if i = n then 
-	  let l1,l2=(div_implicits (n-1) l) in l1,i::l2
-        else 
-	  i::l,[]
-
 let bdize_app c al =
   let impl =
     match c with
@@ -338,52 +436,10 @@ let bdize_app c al =
       | VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
       | _ -> []
   in
-  if impl = [] then 
-    ope("APPLIST", al)
-  else if !print_implicits then 
-    ope("APPLIST", ope("XTRA",[str "!";List.hd al])::List.tl al)
-  else 
-    let largs = List.length al - 1 in
-    let impl = List.rev (filter_until largs impl) in
-    let impl1,impl2=div_implicits largs impl in
-    let al1 = Array.of_list al in
-    List.iter
-      (fun i -> al1.(i) <-
-         ope("XTRA", [str "!"; str "EX"; num i; al1.(i)]))
-      impl2;
-    List.iter
-      (fun i -> al1.(i) <-
-         ope("XTRA",[str "!"; num i; al1.(i)]))
-      impl1;
-    al1.(0) <- ope("XTRA",[str "!"; al1.(0)]);
-    ope("APPLIST",Array.to_list al1)
-
-type optioncast = WithCast | WithoutCast
-
-(* [reference_tree p] pre-computes the variables and de bruijn occurring
-   in a term to avoid a O(n2) factor when computing dependent each time *)
-
-type ref_tree =
-  NODE of (int list * identifier list) * ref_tree list
-
-let combine l =
-  let rec combine_rec = function
-    | [] -> [],[]
-    | NODE ((a,b),_)::l -> 
-        let a',b' = combine_rec l in (list_union a a',list_union b b')
-  in 
-  NODE (combine_rec l,l)
-
-let rec reference_tree p = function
-  | VAR id -> NODE (([],[id]),[])
-  | Rel n  -> NODE (([n-p],[]),[])
-  | DOP0 op -> NODE (([],[]),[])
-  | DOP1(op,c) -> reference_tree p c
-  | DOP2(op,c1,c2) -> combine [reference_tree p c1;reference_tree p c2]
-  | DOPN(op,cl) -> combine (List.map (reference_tree p) (Array.to_list cl))
-  | DOPL(op,cl) -> combine (List.map (reference_tree p) cl)
-  | DLAM(na,c) -> reference_tree (p+1) c 
-  | DLAMV(na,cl) -> combine (List.map (reference_tree (p+1))(Array.to_list cl))
+  if !print_implicits then 
+    ope("APPLISTEXPL", al)
+  else
+    ope("APPLIST", explicitize impl al)
 
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -413,9 +469,16 @@ let computable p k =
   in 
   striprec (k,p)
 
+let ids_of_var cl =
+  List.map
+    (function 
+       | RRef (_,RVar id) -> id
+       | _-> anomaly "ids_of_var")
+    (Array.to_list cl)
+
 (* Main translation function from constr -> ast *)
 
-let old_bdize_depcast opcast at_top env t =
+let old_bdize at_top env t =
   let init_avoid = if at_top then ids_of_env env else [] in
   let rec bdrec avoid env t = match collapse_appl t with
     (* Not well-formed constructions *)
@@ -458,7 +521,7 @@ let old_bdize_depcast opcast at_top env t =
 		      ope("TYPE",
 			  [path_section dummy_loc u.u_sp; num u.u_num]))
 	   | IsCast (c1,c2) ->
-	       if opcast=WithoutCast then 
+	       if !print_casts then 
 		 bdrec avoid env c1 
 	       else 
 		 ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
@@ -497,7 +560,7 @@ let old_bdize_depcast opcast at_top env t =
 		   ((path_section dummy_loc sp)::(num tyi)::(num n)::
 		    (array_map_to_list (bdrec avoid env) cl)))
 	   | IsMutCase (annot,p,c,bl) ->
-	       let synth_type = synthetize_type () in
+	       let synth_type = Detyping.synthetize_type () in
 	       let tomatch = bdrec avoid env c in
 	       begin 
 		 match annot with
@@ -519,7 +582,7 @@ let old_bdize_depcast opcast at_top env t =
 		       else 
 			 bdrec avoid env p 
 		     in
-		     if PrintingIf.active indsp then 
+		     if Detyping.force_if indsp then 
 		       ope("FORCEIF", [ pred; tomatch;
 					bdrec avoid env bl.(0); 
 					bdrec avoid env bl.(1) ])
@@ -531,10 +594,10 @@ let old_bdize_depcast opcast at_top env t =
 			   lcparams bl in
 		       let eqnl = Array.to_list eqnv in
 		       let tag =
-			 if PrintingLet.active indsp then 
+			 if Detyping.force_let indsp then 
 			   "FORCELET" 
 			 else 
-			   "MULTCASE"
+			   "CASES"
 		       in 
 		       ope(tag,pred::asttomatch::eqnl)
 	       end
@@ -601,7 +664,7 @@ let old_bdize_depcast opcast at_top env t =
 	       ope("COFIX", (nvar (string_of_id f))::listdecl))
 
   and bdize_eqn avoid env constructid construct_params branch =
-    let print_underscore = force_wildcard () in
+    let print_underscore = Detyping.force_wildcard () in
     let cnvar = nvar (string_of_id constructid) in
     let rec buildrec nvarlist avoid env = function
 
@@ -654,320 +717,16 @@ let old_bdize_depcast opcast at_top env t =
 
   in
     bdrec init_avoid env t
-
-let lookup_name_as_renamed env t s =
-  let rec lookup avoid env n = function
-      DOP2(Prod,_,DLAM(name,c')) ->
-       (match concrete_name avoid env name c' with
-          (Some id,avoid') -> 
-	    if id=s then (Some n) 
-	    else lookup avoid' (add_rel (Name id,()) env) (n+1) c'
-	  | (None,avoid')    -> lookup avoid' env (n+1) (pop c'))
-     | DOP2(Cast,c,_) -> lookup avoid env n c
-     | _ -> None
-  in lookup (ids_of_env env) env 1 t
-
-let lookup_index_as_renamed t n =
-  let rec lookup n d = function
-      DOP2(Prod,_,DLAM(name,c')) -> 
-	  (match concrete_name [] (gLOB nil_sign) name c' with
-          (Some _,_) -> lookup n (d+1) c'
-        | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
-    | DOP2(Cast,c,_) -> lookup n d c
-    | _ -> None
-  in lookup n 1 t
-
-(*
-Until V6.2.4, similar names were allowed in hypothesis and quantified
-variables of a goal.
-*)
-
-(* $Id$ *)
-
-exception StillDLAM
-
-let rec detype avoid env t =
-  match collapse_appl t with
-    (* Not well-formed constructions *)
-    | DLAM _ | DLAMV _ -> raise StillDLAM
-    (* Well-formed constructions *)
-    | regular_constr -> 
-    (match kind_of_term regular_constr with
-    | IsRel n ->
-      (try match fst (lookup_rel n env) with
-	 | Name id   -> RRef (dummy_loc, RVar id)
-	 | Anonymous -> anomaly "detype: index to an anonymous variable"
-       with Not_found ->
-	 let s = "[REL "^(string_of_int (n - List.length (get_rels env)))^"]"
-	 in RRef (dummy_loc, RVar (id_of_string s)))
-    | IsMeta n -> RRef (dummy_loc,RMeta n)
-    | IsVar id -> RRef (dummy_loc,RVar id)
-    | IsXtra s -> warning "bdize: Xtra should no longer occur in constr";
-	RRef(dummy_loc,RVar (id_of_string ("XTRA"^s)))
-        (* ope("XTRA",((str s):: pl@(List.map detype cl)))*) 
-    | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
-    | IsSort (Type _) -> RSort (dummy_loc,RType)
-    | IsCast (c1,c2) ->
-	RCast(dummy_loc,detype avoid env c1,detype avoid env c2)
-    | IsProd (na,ty,c) -> detype_binder BProd avoid env na ty c
-    | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
-    | IsAppL (f,args) ->
-	RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args)
-    | IsConst (sp,cl) ->
-	RRef(dummy_loc,RConst(sp,ids_of_var (Array.map (detype avoid env) cl)))
-    | IsEvar (ev,cl) ->
-	RRef(dummy_loc,REVar(ev,ids_of_var (Array.map (detype avoid env) cl)))
-    | IsAbst (sp,cl) -> 
-	anomaly "bdize: Abst should no longer occur in constr"
-    | IsMutInd (ind_sp,cl) ->
-	let ids = ids_of_var (Array.map (detype avoid env) cl) in
-	RRef (dummy_loc,RInd (ind_sp,ids))
-    | IsMutConstruct (cstr_sp,cl) ->
-	let ids = ids_of_var (Array.map (detype avoid env) cl) in
-	RRef (dummy_loc,RConstruct (cstr_sp,ids))
-    | IsMutCase (annot,p,c,bl) ->
-	let synth_type = synthetize_type () in
-	let tomatch = detype avoid env c in
-	begin 
-	  match annot with
-(*	  | None -> (* Pas d'annotation --> affichage avec vieux Case *)
-	      warning "Printing in old Case syntax";
-	      ROldCase (dummy_loc,false,Some (detype avoid env p),
-			tomatch,Array.map (detype avoid env) bl)
-	  | Some *) indsp ->
-	      let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
-	      let lc = lc_of_lmis lmis in
-	      let lcparams = Array.map get_params lc in
-	      let k = (nb_prod mip.mind_arity.body) - 
-		      mib.mind_nparams in
-	      let pred = 
-		if synth_type & computable p k & lcparams <> [||] then
-		  None
-		else 
-		  Some (detype avoid env p) 
-	      in
-	      let constructs = 
-		Array.init
-		  (Array.length mip.mind_consnames)
-		  (fun i -> ((indsp,i+1),[] (* on triche *))) in
-	      let eqnv =
-		array_map3 (detype_eqn avoid env) constructs lcparams bl in
-	      let eqnl = Array.to_list eqnv in
-	      let tag =
-		if PrintingLet.active indsp then 
-		  PrintLet 
-		else if PrintingIf.active indsp then 
-		  PrintIf 
-		else 
-		  PrintCases
-	      in 
-	      RCases (dummy_loc,tag,pred,[tomatch],eqnl)
-	end
-	
-    | IsFix (nv,n,cl,lfn,vt) -> detype_fix (RFix (nv,n)) avoid env cl lfn vt
-    | IsCoFix (n,cl,lfn,vt)  -> detype_fix (RCofix n) avoid env cl lfn vt)
-
-and detype_fix fk avoid env cl lfn vt =
-  let lfi = List.map (fun id -> next_name_away id avoid) lfn in
-  let def_avoid = lfi@avoid in
-  let def_env =
-    List.fold_left (fun env id -> add_rel (Name id,()) env) env lfi in
-  RRec(dummy_loc,fk,Array.of_list lfi,Array.map (detype avoid env) cl,
-       Array.map (detype def_avoid def_env) vt)
-
-
-and detype_eqn avoid env constr_id construct_params branch =
-  let make_pat x avoid env b ids =
-    if not (force_wildcard ()) or (dependent (Rel 1) b) then
-      let id = next_name_away_with_default "x" x avoid in
-      PatVar (dummy_loc,Name id),id::avoid,(add_rel (Name id,()) env),id::ids
-    else 
-      PatVar (dummy_loc,Anonymous),avoid,(add_rel (Anonymous,()) env),ids
-  in
-  let rec buildrec ids patlist avoid env = function
-    | _::l, DOP2(Lambda,_,DLAM(x,b)) -> 
-	let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
-        buildrec new_ids (pat::patlist) new_avoid new_env (l,b)
-
-    | l   , DOP2(Cast,b,_) ->    (* Oui, il y a parfois des cast *)
-	buildrec ids patlist avoid env (l,b)
-	  
-    | x::l, b -> (* eta-expansion : n'arrivera plus lorsque tous les
-                   termes seront construits à partir de la syntaxe Cases *)
-	(* nommage de la nouvelle variable *)
-	let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
-        let pat,new_avoid,new_env,new_ids = make_pat x avoid env new_b ids in
-	buildrec new_ids (pat::patlist) new_avoid new_env (l,new_b)
-	  
-    | []  , rhs	-> 
-	(ids, [PatCstr(dummy_loc, constr_id, List.rev patlist,Anonymous)],
-	 detype avoid env rhs)
-  in 
-  buildrec [] [] avoid env (construct_params,branch)
-
-and detype_binder bk avoid env na ty c =
-  let na',avoid' = match concrete_name avoid env na c with
-    | (Some id,l') -> (Name id), l'
-    | (None,l')    -> Anonymous, l' in
-  RBinder (dummy_loc,bk,
-	   na',detype [] env ty,
-	   detype avoid' (add_rel (na',()) env) c)
-
-let ast_dependent na aty =
-  match na with
-    | Name id -> occur_var_ast (string_of_id id) aty
-    | Anonymous -> false
-
-let implicit_of_ref = function
-  | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
-  | RInd (indid,_) -> inductive_implicits_list indid
-  | RConst (sp,_) -> constant_implicits_list sp
-  | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
-  | _ -> []
-
-let ast_of_app impl f args =
-  if impl = [] then 
-    ope("APPLIST", f::args)
-  else if !print_implicits then 
-    ope("APPLISTEXPL", (f::args))
-  else 
-    let largs = List.length args in
-    let impl = List.rev (filter_until largs impl) in
-    let impl1,impl2=div_implicits largs impl in
-    let al1 = Array.of_list args in
-    List.iter
-      (fun i -> al1.(i) <-
-         ope("EXPL", [str "EX"; num i; al1.(i)]))
-      impl2;
-    List.iter
-      (fun i -> al1.(i) <-
-         ope("EXPL",[num i; al1.(i)]))
-      impl1;
-    (* On laisse les implicites, à charge du PP de ne pas les imprimer *)
-    ope("APPLISTEXPL",f::(Array.to_list al1))
-
-let rec ast_of_raw = function
-  | RRef (_,ref) -> ast_of_ref ref
-  | RApp (_,f,args) ->
-      let astf = ast_of_raw f in
-      let astargs = List.map ast_of_raw args in
-      (match f with 
-	 | RRef (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs
-	 | _           -> ast_of_app [] astf astargs)
-  | RBinder (_,BProd,Anonymous,t,c) ->
-      (* Anonymous product are never factorized *)
-      ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
-  | RBinder (_,bk,na,t,c) ->
-      let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
-      let tag = match bk with
-	  (* LAMBDA et LAMBDALIST se comportent pareil *)
-	| BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST"
-	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
-	  (* non dépendant, pour isoler l'implication; peut-être un *)
-	  (* constructeur ARROW serait-il plus justifié ? *) 
-	| BProd -> if n=1 then "PROD" else "PRODLIST" 
-      in
-      ope(tag,[ast_of_raw t;a])
-
-  | RCases (_,printinfo,typopt,tml,eqns) ->
-      let pred = ast_of_rawopt typopt in
-      let tag = match printinfo with
-	| PrintIf -> "FORCEIF"
-	| PrintLet -> "FORCELET"
-	| PrintCases -> "MULTCASE" 
-      in
-      let asttomatch = ope("TOMATCH", List.map ast_of_raw tml) in
-      let asteqns = List.map ast_of_eqn eqns in 
-      ope(tag,pred::asttomatch::asteqns)
-	
-  | ROldCase (_,isrec,typopt,tm,bv) ->
-      warning "Old Case syntax";
-      ope("MUTCASE",(ast_of_rawopt typopt)
-	    ::(ast_of_raw tm)
-	    ::(Array.to_list (Array.map ast_of_raw bv)))
-  | RRec (_,fk,idv,tyv,bv) ->
-      let alfi = Array.map ast_of_ident idv in
-      (match fk with
-	 | RFix (nv,n) ->
-             let rec split_lambda binds = function
-	       | (0, t) -> (binds,ast_of_raw t)
-	       | (n, RBinder(_,BLambda,na,t,b)) ->
-		   let bind = ope("BINDER",[ast_of_raw t;ast_of_name na]) in
-		   split_lambda (bind::binds) (n-1,b)
-	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
-	     let rec split_product = function
-	       | (0, t) -> ast_of_raw t
-	       | (n, RBinder(_,BProd,na,t,b)) -> split_product (n-1,b)
-	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
-	     let listdecl = 
-	       Array.mapi
-		 (fun i fi ->
-		    let (lparams,astdef) = split_lambda [] (nv.(i)+1,bv.(i)) in
-		    let asttyp = split_product (nv.(i)+1,tyv.(i)) in
-		    ope("FDECL",
-		       	[fi; ope ("BINDERS",List.rev lparams); 
-			 asttyp; astdef]))
-		 alfi
-	     in 
-	     ope("FIX", alfi.(n)::(Array.to_list listdecl))
-	 | RCofix n -> 
-	     let listdecl =
-               Array.mapi 
-		 (fun i fi ->
-		    ope("CFDECL",[fi; ast_of_raw tyv.(i); ast_of_raw bv.(i)]))
-		 alfi
-	     in 
-	     ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
-
-  | RSort (_,s) ->
-      (match s with
-	 | RProp Null -> ope("PROP",[])
-	 | RProp Pos -> ope("SET",[])
-	 | RType -> ope("TYPE",[]))
-  | RHole _ -> ope("ISEVAR",[])
-  | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
-	
-and ast_of_eqn (idl,pl,c) =
-  ope("EQN", (ast_of_raw c)::(List.map ast_of_pattern pl))
-
-and ast_of_rawopt = function
-  | None -> (str "SYNTH")
-  | Some p -> ast_of_raw p
-
-and factorize_binder n oper na aty c =
-  let (p,body) = match c with
-    | RBinder(_,oper',na',ty',c')
-	when (oper = oper') & (aty = ast_of_raw ty')
-	  & not (ast_dependent na aty) (* To avoid na in ty' escapes scope *)
-	  & not (na' = Anonymous & oper = BProd)
-	  -> factorize_binder (n+1) oper na' aty c'
-    | _ -> (n,ast_of_raw c)
-  in
-  (p,slam(stringopt_of_name na, body))
-
-let ast_of_rawconstr = ast_of_raw
+(* FIN TO EJECT *)
+(******************************************************************)
        
 let bdize at_top env t =
+  let t' =
+    if !print_casts then t
+    else Reduction.strong (fun _ _ -> strip_outer_cast)
+      Environ.empty_env Evd.empty t in
   try
     let avoid = if at_top then ids_of_env env else [] in
-    ast_of_raw (detype avoid env t)
-  with StillDLAM -> 
-    old_bdize_depcast WithoutCast at_top env t
-
-(* En attendant que strong aille dans term.ml *)
-let rec strong whdfun t = 
-  match whdfun t with 
-    | DOP0 _ as t -> t
-	(* Cas ad hoc *)
-    | DOP1(oper,c) -> DOP1(oper,strong whdfun c)
-    | DOP2(oper,c1,c2) -> DOP2(oper,strong whdfun c1,strong whdfun c2)
-    | DOPN(oper,cl) -> DOPN(oper,Array.map (strong whdfun) cl)
-    | DOPL(oper,cl) -> DOPL(oper,List.map (strong whdfun) cl)
-    | DLAM(na,c) -> DLAM(na,strong whdfun c)
-    | DLAMV(na,c) -> DLAMV(na,Array.map (strong whdfun) c)
-    | VAR _ as t -> t
-    | Rel _ as t -> t
-
-let bdize_no_casts at_top env t = bdize at_top env (strong strip_outer_cast t) 
-			   
-
+    ast_of_raw (Detyping.detype avoid env t')
+  with Detyping.StillDLAM ->
+    old_bdize at_top env t'
diff --git a/parsing/termast.mli b/parsing/termast.mli
index d0c0d237a..29ff2d19c 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -8,16 +8,28 @@ open Sign
 open Rawterm
 (*i*)
 
-val print_implicits : bool ref
-
 (* Translation of pattern, rawterm and term into syntax trees for printing *)
 
 val ast_of_pattern : pattern -> Coqast.t
 val ast_of_rawconstr : rawconstr -> Coqast.t
 val bdize : bool -> unit assumptions -> constr -> Coqast.t
+
+(*i C'est bdize qui sait maintenant s'il faut afficher les casts ou pas
 val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
+i*)
+
+val ast_of_constant     : constant -> Coqast.t
+val ast_of_existential  : existential -> Coqast.t
+val ast_of_constructor  : constructor -> Coqast.t
+val ast_of_inductive    : inductive -> Coqast.t
+
+(* For debugging *)
+val print_implicits : bool ref
+val print_casts : bool ref
+val print_arguments : bool ref
+val print_coercions : bool ref
 
-(* look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_renamed :
-  unit assumptions -> constr -> identifier -> int option
-val lookup_index_as_renamed : constr -> int -> int option
+val with_casts : ('a -> 'b) -> 'a -> 'b
+val with_implicits : ('a -> 'b) -> 'a -> 'b
+val with_arguments : ('a -> 'b) -> 'a -> 'b
+val with_coercions : ('a -> 'b) -> 'a -> 'b