Restructuration et simplification des fonctions d'affichage, de détypage

et d'"externalisation"; standardisation du nom des fonctions d'affichage


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

9 files changed, 215 insertions, 232 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 2f2f0773b4..5a969490d9 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -20,6 +20,8 @@ open Topconstr
 open Term
 open Pattern
 open Rawterm
+open Constrextern
+open Termops
 (*i*)
 
 let sep_p = fun _ -> str"."
@@ -124,6 +126,10 @@ let pr_sort = function
   | RProp Term.Pos -> str "Set"
   | RType u -> str "Type" ++ pr_opt pr_universe u
 
+let pr_id = pr_id
+let pr_name = pr_name
+let pr_qualid = pr_qualid
+
 let pr_expl_args pr (a,expl) =
   match expl with
   | None -> pr (lapp,L) a
@@ -140,12 +146,6 @@ let pr_opt_type_spc pr = function
   | CHole _ -> mt ()
   | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
-let pr_id = pr_id
-
-let pr_name = function
-  | Anonymous -> str"_"
-  | Name id -> pr_id id
-
 let pr_lident (b,_ as loc,id) =
   if loc <> dummy_loc then
     let (b,_) = unloc loc in
@@ -263,8 +263,6 @@ let rec extract_lam_binders = function
       LocalRawAssum (nal,t) :: bl, c
   | c -> [], c
     
-let pr_global vars ref = pr_global_env vars ref
-
 let split_lambda = function
   | CLambdaN (loc,[[na],t],c) -> (na,t,c)
   | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
@@ -588,20 +586,6 @@ and pr_dangling_with_for sep inherited a =
 
 let pr = pr mt
 
-let rec abstract_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
-      (abstract_constr_expr c bl)
-      
-let rec prod_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
-      (prod_constr_expr c bl)
-
 let rec strip_context n iscast t =
   if n = 0 then
     [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t
@@ -631,34 +615,15 @@ let rec strip_context n iscast t =
     | CLetIn (_,na,b,c) -> 
 	let bl', c = strip_context (n-1) iscast c in
 	LocalRawDef (na,b) :: bl', c
-    | _ -> anomaly "ppconstrnew: strip_context"
+    | _ -> anomaly "strip_context"
 
-let pr_constr_env env c = pr lsimple c
-let pr_lconstr_env env c = pr ltop c
-let pr_constr c = pr_constr_env (Global.env()) c
-let pr_lconstr c = pr_lconstr_env (Global.env()) c
+let pr_constr_expr c = pr lsimple c
+let pr_lconstr_expr c = pr ltop c
+let pr_pattern_expr c = pr lsimple c
+let pr_cases_pattern_expr = pr_patt ltop
 
 let pr_binders = pr_undelimited_binders (pr ltop)
 
-let pr_lconstr_env_n env iscast bl c = bl, pr ltop c
-let pr_type c = pr ltop c
-
-let transf_pattern env c =
-  if Options.do_translate() then
-    Constrextern.extern_rawconstr (Termops.vars_of_env env)
-      (Constrintern.for_grammar
-	(Constrintern.intern_gen false ~allow_soapp:true Evd.empty env) c)
-  else c
-
-let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c)
-
-let pr_rawconstr_env env c =
-  pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
-let pr_lrawconstr_env env c =
-  pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
-
-let pr_cases_pattern = pr_patt ltop
-
 let pr_pattern_occ prc = function
     ([],c) -> prc c
   | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++
@@ -669,10 +634,6 @@ let pr_unfold_occ pr_ref = function
   | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++
                        hov 0 (prlist_with_sep spc int nl))
 
-let pr_qualid qid = str (string_of_qualid qid)
-
-let pr_arg pr x = spc () ++ pr x
-
 let pr_red_flag pr r =
   (if r.rBeta then pr_arg str "beta" else mt ()) ++
   (if r.rIota then pr_arg str "iota" else mt ()) ++
@@ -726,17 +687,3 @@ let rec pr_may_eval test prc prlc pr2 = function
   | ConstrTerm c -> prc c
 
 let pr_may_eval a = pr_may_eval (fun _ -> false) a
-
-(** constr printers *)
-
-let pr_term_env env  c = pr lsimple (Constrextern.extern_constr false env c)
-let pr_lterm_env env c = pr ltop    (Constrextern.extern_constr false env c)
-let pr_term  c = pr_term_env  (Global.env()) c
-let pr_lterm c = pr_lterm_env (Global.env()) c
-
-let pr_constr_pattern_env env c =
-  pr lsimple (Constrextern.extern_pattern env Termops.empty_names_context c)
-
-let pr_constr_pattern t =
-  pr lsimple
-    (Constrextern.extern_pattern (Global.env()) Termops.empty_names_context t)
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index e6af0e369e..51fbfcb262 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -30,15 +30,17 @@ val extract_def_binders :
 val split_fix :
   int -> constr_expr -> constr_expr -> 
   local_binder list *  constr_expr * constr_expr
-val pr_binders : local_binder list -> std_ppcmds
 
 val prec_less : int -> int * Ppextend.parenRelation -> bool
  
-val pr_global : Idset.t -> global_reference -> std_ppcmds
- 
 val pr_tight_coma : unit -> std_ppcmds
+
 val pr_located :
   ('a -> std_ppcmds) -> 'a located -> std_ppcmds
+val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_metaid : identifier -> std_ppcmds
+
 val pr_lident : identifier located -> std_ppcmds
 val pr_lname : name located -> std_ppcmds
 
@@ -48,40 +50,22 @@ val pr_sep_com :
   (unit -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) ->
   constr_expr -> std_ppcmds
-val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+
 val pr_id : identifier -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
-val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-val pr_metaid : identifier -> std_ppcmds
+
 val pr_red_expr :
   ('a -> std_ppcmds) * ('a -> std_ppcmds) *  ('b -> std_ppcmds) ->
     ('a,'b) red_expr_gen -> std_ppcmds
-
-val pr_sort : rawsort -> std_ppcmds
-val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds
-val pr_constr : constr_expr -> std_ppcmds
-val pr_lconstr : constr_expr -> std_ppcmds
-val pr_constr_env : env -> constr_expr -> std_ppcmds
-val pr_lconstr_env : env -> constr_expr -> std_ppcmds
-val pr_type : constr_expr -> std_ppcmds
-val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
 val pr_may_eval :
-  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
-    -> std_ppcmds
-val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
-val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
-
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+    ('a,'b) may_eval -> std_ppcmds
 
-val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
-val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
-
-(** constr printers *)
-
-val pr_term_env : env -> constr -> std_ppcmds
-val pr_lterm_env : env -> constr -> std_ppcmds
-val pr_term : constr -> std_ppcmds
-val pr_lterm : constr -> std_ppcmds
+val pr_sort : rawsort -> std_ppcmds
 
-val pr_constr_pattern_env : env -> Pattern.constr_pattern -> std_ppcmds
-val pr_constr_pattern : Pattern.constr_pattern -> std_ppcmds
+val pr_binders : local_binder list -> std_ppcmds
+val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+val pr_constr_expr : constr_expr -> std_ppcmds
+val pr_lconstr_expr : constr_expr -> std_ppcmds
+val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 8476ccf2a7..c2029dde5b 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -20,6 +20,7 @@ open Libnames
 open Pattern
 open Ppextend
 open Ppconstr
+open Printer
 
 let pr_global x = Nametab.pr_global_env Idset.empty x
 
@@ -919,9 +920,9 @@ let drop_env f _env = f
 
 let rec raw_printers =
     (pr_raw_tactic_level, 
-     drop_env pr_constr,
-     drop_env pr_lconstr,
-     pr_pattern,
+     drop_env pr_constr_expr,
+     drop_env pr_lconstr_expr,
+     pr_pattern_expr,
      drop_env pr_reference,
      drop_env pr_reference,
      pr_reference,
@@ -958,8 +959,8 @@ and pr_glob_match_rule env t =
 let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) =
   make_pr_tac
     (pr_glob_tactic_level,
-     pr_term_env,
-     pr_lterm_env,
+     pr_constr_env,
+     pr_lconstr_env,
      pr_constr_pattern,
      pr_evaluable_reference_env,
      pr_inductive,
@@ -976,10 +977,8 @@ let _ = Tactic_debug.set_tactic_printer
   (fun x -> pr_glob_tactic (Global.env()) x)
 
 let _ = Tactic_debug.set_match_pattern_printer
-  (fun env hyp ->
-    pr_match_pattern
-      (Printer.pr_pattern_env env (Termops.names_of_rel_context env)) hyp)
+  (fun env hyp -> pr_match_pattern (pr_constr_pattern_env env) hyp)
 
 let _ = Tactic_debug.set_match_rule_printer
   (fun rl ->
-    pr_match_rule false (pr_glob_tactic (Global.env())) Printer.pr_pattern rl)
+    pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 41c391802c..2444b1be9e 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -26,7 +26,7 @@ open Topconstr
 open Decl_kinds
 open Tacinterp
 
-let pr_spc_type = pr_sep_com spc pr_type
+let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
 let pr_lident (b,_ as loc,id) =
   if loc <> dummy_loc then
@@ -65,8 +65,8 @@ let pr_raw_tactic_env l env t =
 
 let pr_gen env t =
   pr_raw_generic 
-    pr_constr
-    pr_lconstr
+    pr_constr_expr
+    pr_lconstr_expr
     (pr_raw_tactic_level env) pr_reference t
 
 let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac
@@ -507,11 +507,11 @@ let rec pr_vernac = function
         | DefineBody (bl,red,body,d) ->
             let ty = match d with
               | None -> mt()
-              | Some ty -> spc() ++ str":" ++ pr_sep_com spc pr_lconstr ty
+              | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
 	    in
             (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
         | ProveBody (bl,t) ->
-            (pr_binders_arg bl, str" :" ++ pr_spc_type t, None) in
+            (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
       let (binds,typ,c) = pr_def_body b in
       hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++
       (match c with
@@ -523,7 +523,7 @@ let rec pr_vernac = function
       (match bl with
         | [] -> mt()
         | _ -> pr_binders bl ++ spc())
-      ++ str":" ++ pr_spc_type c)
+      ++ str":" ++ pr_spc_lconstr c)
   | VernacEndProof Admitted -> str"Admitted"
   | VernacEndProof (Proved (opac,o)) -> (match o with
     | None -> if opac then str"Qed" else str"Defined"
@@ -536,13 +536,13 @@ let rec pr_vernac = function
       let n = List.length (List.flatten (List.map fst (List.map snd l))) in
       hov 2
         (pr_assumption_token (n > 1) stre ++ spc() ++ 
-	 pr_ne_params_list pr_type l)
+	 pr_ne_params_list pr_lconstr_expr l)
   | VernacInductive (f,l) ->
 
       let pr_constructor (coe,(id,c)) =
         hov 2 (pr_lident id ++ str" " ++
                (if coe then str":>" else str":") ++
-                pr_sep_com spc pr_type c) in
+                pr_spc_lconstr c) in
       let pr_constructor_list l = match l with
         | [] -> mt()
         | _ ->
@@ -554,7 +554,7 @@ let rec pr_vernac = function
 	hov 0 (
           str key ++ spc() ++
           pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
-	  spc() ++ pr_type s ++ 
+	  spc() ++ pr_lconstr_expr s ++ 
 	  str" :=") ++ pr_constructor_list lc ++ 
 	pr_decl_notation pr_constr ntn in
 
@@ -584,7 +584,7 @@ let rec pr_vernac = function
                 spc() ++ str "{struct " ++ pr_name name ++ str"}"
               else mt() in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
-            ++ pr_type_option (fun c -> spc() ++ pr_type c) type_
+            ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
             ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++ 
 	    pr_decl_notation pr_constr ntn
       in
@@ -599,7 +599,7 @@ let rec pr_vernac = function
               else ([],def,c) in
         let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
-        spc() ++ pr_type c ++
+        spc() ++ pr_lconstr_expr c ++
         str" :=" ++ brk(1,1) ++ pr_lconstr def in
       let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
       hov 1 (str start ++ spc() ++
@@ -614,20 +614,20 @@ let rec pr_vernac = function
         | (oc,AssumExpr (id,t)) ->
             hov 1 (pr_lname id ++
             (if oc then str" :>" else str" :") ++ spc() ++
-            pr_type t)
+            pr_lconstr_expr t)
         | (oc,DefExpr(id,b,opt)) -> (match opt with
 	    | Some t ->
                 hov 1 (pr_lname id ++
                 (if oc then str" :>" else str" :") ++ spc() ++
-                pr_type t ++ str" :=" ++ pr_lconstr b)
+                pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
 	    | None ->
                 hov 1 (pr_lname id ++ str" :=" ++ spc() ++
                 pr_lconstr b)) in
       hov 2
         (str (if b then "Record" else "Structure") ++
          (if oc then str" > " else str" ") ++ pr_lident name ++ 
-          pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++ 
-	  str" := " ++
+          pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ 
+	  pr_lconstr_expr s ++ str" := " ++
          (match c with
            | None -> mt()
            | Some sc -> pr_lident sc) ++
@@ -732,7 +732,7 @@ let rec pr_vernac = function
 	    (* Rec by default *) str "Ltac ") ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacHints (local,dbnames,h) ->
-      pr_hints local dbnames h pr_constr pr_pattern
+      pr_hints local dbnames h pr_constr pr_pattern_expr
   | VernacSyntacticDefinition (id,c,local,onlyparsing) ->
       hov 2
         (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++
@@ -749,7 +749,8 @@ let rec pr_vernac = function
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
         str (if List.length idl > 1 then "s " else " ") ++
-        prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_type c)
+        prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++
+        pr_lconstr c)
   | VernacSetOpacity (fl,l) ->
       hov 1 ((if fl then str"Opaque" else str"Transparent") ++
              spc() ++ prlist_with_sep sep pr_reference l)
@@ -808,7 +809,7 @@ let rec pr_vernac = function
 	| PrintAbout qid -> str"About" ++ spc()  ++ pr_reference qid
 	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
       in pr_printable p
-  | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern
+  | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr
   | VernacLocate loc -> 
       let pr_locate =function
 	| LocateTerm qid ->  pr_reference qid
@@ -852,4 +853,4 @@ and pr_extend s cl =
 
 in pr_vernac
 
-let pr_vernac v = make_pr_vernac pr_constr pr_lconstr v ++ sep_end ()
+let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end ()
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 821679b4f8..1bd1109266 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -70,7 +70,7 @@ let print_ref reduce ref =
       let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
       in it_mkProd_or_LetIn ccl ctx 
     else typ in
-  hov 0 (pr_global ref ++ str " :" ++ spc () ++ prtype typ) ++ fnl ()
+  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) ++ fnl ()
 
 let print_argument_scopes = function
   | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl()
@@ -225,8 +225,8 @@ let print_located_qualid ref =
 (**** Printing declarations and judgments *)
 
 let print_typed_value_in_env env (trm,typ) =
-  (prterm_env env trm ++ fnl () ++
-     str "     : " ++ prtype_env env typ ++ fnl ())
+  (pr_lconstr_env env trm ++ fnl () ++
+     str "     : " ++ pr_ltype_env env typ ++ fnl ())
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
 
@@ -239,20 +239,20 @@ let print_safe_judgment env j =
   print_typed_value_in_env env (trm, typ)
     
 (* To be improved; the type should be used to provide the types in the
-   abstractions. This should be done recursively inside prterm, so that
+   abstractions. This should be done recursively inside pr_lconstr, so that
    the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
    synthesizes the type nat of the abstraction on u *)
 
 let print_named_def name body typ =
-  let pbody = prterm body in
-  let ptyp = prtype typ in
+  let pbody = pr_lconstr body in
+  let ptyp = pr_ltype typ in
   (str "*** [" ++ str name ++ str " " ++
      hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
 	      str ":" ++ brk (1,2) ++ ptyp) ++
 	   str "]" ++ fnl ())
 
 let print_named_assum name typ =
-  (str "*** [" ++ str name ++ str " : " ++ prtype typ ++ str "]" ++ fnl ())
+  (str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" ++ fnl ())
 
 let print_named_decl (id,c,typ) =
   let s = string_of_id id in
@@ -272,7 +272,7 @@ let print_params env params =
 let print_constructors envpar names types =
   let pc =
     prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
-      (fun (id,c) -> pr_id id ++ str " : " ++ prterm_env envpar c)
+      (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
       (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
   in 
   hv 0 (str "  " ++ pc)
@@ -295,7 +295,7 @@ let print_one_inductive (sp,tyi) =
   let envpar = push_rel_context params env in
   hov 0 (
     pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++
-    str ": " ++ prterm_env envpar arity ++ str " :=") ++
+    str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
   brk(0,2) ++ print_constructors envpar cstrnames cstrtypes
 
 let pr_mutual_inductive finite indl =
@@ -319,11 +319,11 @@ let print_section_variable sp =
   print_name_infos (VarRef sp)
 
 let print_body = function
-  | Some lc  -> prterm (Declarations.force lc)
+  | Some lc  -> pr_lconstr (Declarations.force lc)
   | None -> (str"<no body>")
 
 let print_typed_body (val_0,typ) =
-  (print_body val_0 ++ fnl () ++ str "     : " ++ prtype typ ++ fnl ())
+  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ ++ fnl ())
 
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
@@ -333,11 +333,11 @@ let print_constant with_values sep sp =
     match val_0 with 
     | None -> 
 	str"*** [ " ++ 
-	print_basename sp ++ str " : " ++ cut () ++ prtype typ ++ 
+	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ 
 	str" ]" ++ fnl ()
     | _ -> 
 	print_basename sp ++ str sep ++ cut () ++
-	(if with_values then print_typed_body (val_0,typ) else prtype typ) ++
+	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ) ++
 	fnl ())
 
 let print_constant_with_infos sp =
@@ -349,7 +349,7 @@ let print_syntactic_def sep kn =
   let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in
   let c = Syntax_def.search_syntactic_definition dummy_loc kn in 
   str "Notation " ++ pr_qualid qid ++ str sep ++ 
-  Constrextern.without_symbols pr_rawterm c ++ fnl ()
+  Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
 
 let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
   let tag = object_tag lobj in
@@ -545,7 +545,7 @@ let inspect depth =
 
 open Classops
 
-let print_coercion_value v = prterm (get_coercion_value v)
+let print_coercion_value v = pr_lconstr (get_coercion_value v)
 
 let print_class i =
   let cl,_ = class_info_from_index i in
@@ -588,7 +588,7 @@ let print_path_between cls clt =
 
 let print_canonical_projections () =
   prlist_with_sep pr_fnl (fun ((r1,r2),o) -> 
-    pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ prterm o.o_DEF ++ str " )")
+    pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
     (canonical_projections ())
 
 (*************************************************************************)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 7efea20a86..782cd3b4a3 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -26,65 +26,98 @@ open Proof_type
 open Refiner
 open Pfedit
 open Ppconstr
+open Constrextern
 
 let emacs_str s = if !Options.print_emacs then s else "" 
 
 (**********************************************************************)
-(* Generic printing: choose old or new printers *)
+(** Terms                                                             *)
+
+  (* [at_top] means ids of env must be avoided in bound variables *)
+let pr_constr_core at_top env t =
+  pr_constr_expr (extern_constr at_top env t)
+let pr_lconstr_core at_top env t =
+  pr_lconstr_expr (extern_constr at_top env t)
+
+let pr_lconstr_env_at_top env = pr_lconstr_core true env
+let pr_lconstr_env env = pr_lconstr_core false env
+let pr_constr_env env = pr_constr_core false env
+
+  (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
+let pr_lconstr t = pr_lconstr_env (Global.env()) t
+let pr_constr t = pr_constr_env (Global.env()) t
+
+let pr_type_core at_top env t =
+  pr_constr_expr (extern_type at_top env t)
+let pr_ltype_core at_top env t =
+  pr_lconstr_expr (extern_type at_top env t)
+
+let pr_ltype_env_at_top env = pr_ltype_core true env
+let pr_ltype_env env = pr_ltype_core false env
+let pr_type_env env = pr_type_core false env
+
+let pr_ltype t = pr_ltype_env (Global.env()) t
+let pr_type t = pr_type_env (Global.env()) t
+
+let pr_ljudge_env env j =
+  (pr_lconstr_env env j.uj_val, pr_lconstr_env env j.uj_type)
+
+let pr_ljudge j = pr_ljudge_env (Global.env()) j
+
+let pr_lrawconstr_env env c =
+  pr_lconstr_expr (extern_rawconstr (vars_of_env env) c)
+let pr_rawconstr_env env c = 
+  pr_constr_expr (extern_rawconstr (vars_of_env env) c)
+
+let pr_lrawconstr c =
+  pr_lconstr_expr (extern_rawconstr Idset.empty c)
+let pr_rawconstr c =
+  pr_constr_expr (extern_rawconstr Idset.empty c)
 
-(* [at_top] means ids of env must be avoided in bound variables *)
-let prterm_core at_top env t =
-  pr_lconstr (Constrextern.extern_constr at_top env t)
-let prtype_core at_top env t =
-  pr_lconstr (Constrextern.extern_type at_top env t)
 let pr_cases_pattern t =
-  pr_cases_pattern (Constrextern.extern_cases_pattern Idset.empty t)
-let pr_pattern_env tenv env t =
-  pr_constr (Constrextern.extern_pattern tenv env t)
+  pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
+
+let pr_constr_pattern_env env c =
+  pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c)
+let pr_constr_pattern t =
+  pr_constr_expr (extern_constr_pattern empty_names_context t)
+
+let _ = Termops.set_print_constr pr_lconstr_env
 
 (**********************************************************************)
-(* Derived printers *)
-  
-let prterm_env_at_top env = prterm_core true env
-let prterm_env env = prterm_core false env
-let prtype_env_at_top env = prtype_core true env
-let prtype_env env = prtype_core false env
-let prjudge_env env j =
-  (prterm_env env j.uj_val, prterm_env env j.uj_type)
-
-(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
-let prterm t = prterm_env (Global.env()) t
-let prtype t = prtype_env (Global.env()) t
-let prjudge j = prjudge_env (Global.env()) j
-
-let _ = Termops.set_print_constr prterm_env
-
-let pr_constant env cst = prterm_env env (mkConst cst)
-let pr_existential env ev = prterm_env env (mkEvar ev)
-let pr_inductive env ind = prterm_env env (mkInd ind)
-let pr_constructor env cstr = prterm_env env (mkConstruct cstr)
+(* Global references *)
+
+let pr_global_env env ref =
+  (* Il est important de laisser le let-in, car les streams s'évaluent
+  paresseusement : il faut forcer l'évaluation pour capturer
+  l'éventuelle levée d'une exception (cela arrive dans le debugger) *)
+  let s = string_of_qualid (shortest_qualid_of_global env ref) in
+  (str s)
+
 let pr_global = pr_global_env Idset.empty
+
+let pr_constant env cst = pr_global_env (vars_of_env env) (ConstRef cst)
+let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
+let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
+
 let pr_evaluable_reference ref =
  let ref' = match ref with
   | EvalConstRef const -> ConstRef const
   | EvalVarRef sp -> VarRef sp in
  pr_global ref'
 
-let pr_rawterm t =
-  pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)
-
-open Pattern
-
-let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t
+(**********************************************************************)
+(* Contexts and declarations                                          *)
 
 let pr_var_decl env (id,c,typ) =
   let pbody = match c with
     | None ->  (mt ())
     | Some c ->
 	(* Force evaluation *) 
-	let pb = prterm_env env c in
+	let pb = pr_lconstr_env env c in
 	(str" := " ++ pb ++ cut () ) in
-  let pt = prtype_env env typ in
+  let pt = pr_ltype_env env typ in
   let ptyp = (str" : " ++ pt) in
   (pr_id id ++ hov 0 (pbody ++ ptyp))
 
@@ -93,9 +126,9 @@ let pr_rel_decl env (na,c,typ) =
     | None -> mt ()
     | Some c ->
 	(* Force evaluation *) 
-	let pb = prterm_env env c in
+	let pb = pr_lconstr_env env c in
 	(str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = prtype_env env typ in
+  let ptyp = pr_ltype_env env typ in
   match na with
   | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
   | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
@@ -190,7 +223,7 @@ let pr_context_of env = match Options.print_hyps_limit () with
 let pr_goal g =
   let env = evar_env g in
   let penv = pr_context_of env in
-  let pc = prtype_env_at_top env g.evar_concl in
+  let pc = pr_ltype_env_at_top env g.evar_concl in
   str"  " ++ hv 0 (penv ++ fnl () ++
 		   str (emacs_str (String.make 1 (Char.chr 253)))  ++
                    str "============================" ++ fnl ()  ++
@@ -199,14 +232,14 @@ let pr_goal g =
 (* display the conclusion of a goal *)
 let pr_concl n g =
   let env = evar_env g in
-  let pc = prtype_env_at_top env g.evar_concl in
+  let pc = pr_ltype_env_at_top env g.evar_concl in
   str (emacs_str (String.make 1 (Char.chr 253)))  ++
   str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl = 
   let ps = pr_named_context_of (evar_env gl) in
-  let pc = prterm gl.evar_concl in
+  let pc = pr_lconstr gl.evar_concl in
   hov 0 (str"["  ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]")
 
 (* Print an enumerated list of existential variables *)
@@ -284,12 +317,6 @@ let pr_nth_open_subgoal n =
 
 (* Elementary tactics *)
 
-let print_constr8 t =
-  pr_constr (Constrextern.extern_constr false (Global.env()) t)
-
-let print_lconstr8 t =
-  pr_lconstr (Constrextern.extern_constr false (Global.env()) t)
-
 let pr_prim_rule = function
   | Intro id -> 
       str"intro " ++ pr_id id
@@ -299,9 +326,9 @@ let pr_prim_rule = function
 	
   | Cut (b,id,t) ->
       if b then
-        (str"assert " ++ print_constr8 t)
+        (str"assert " ++ pr_constr t)
       else
-        (str"cut " ++ print_constr8 t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
+        (str"cut " ++ pr_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
 	
   | FixRule (f,n,[]) ->
       (str"fix " ++ pr_id f ++ str"/" ++ int n)
@@ -309,7 +336,7 @@ let pr_prim_rule = function
   | FixRule (f,n,others) -> 
       let rec print_mut = function
 	| (f,n,ar)::oth -> 
-           pr_id f ++ str"/" ++ int n ++ str" : " ++ print_lconstr8 ar ++ print_mut oth
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
         | [] -> mt () in
       (str"fix " ++ pr_id f ++ str"/" ++ int n ++
          str" with " ++ print_mut others)
@@ -320,22 +347,22 @@ let pr_prim_rule = function
   | Cofix (f,others) ->
       let rec print_mut = function
 	| (f,ar)::oth ->
-	  (pr_id f ++ str" : " ++ print_lconstr8 ar ++ print_mut oth)
+	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
         | [] -> mt () in
       (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
 
   | Refine c -> 
       str(if occur_meta c then "refine " else "exact ") ++
-      Constrextern.with_meta_as_hole print_constr8 c
+      Constrextern.with_meta_as_hole pr_constr c
       
   | Convert_concl (c,_) ->
-      (str"change "  ++ print_constr8 c)
+      (str"change "  ++ pr_constr c)
       
   | Convert_hyp (id,None,t) ->
-      (str"change "  ++ print_constr8 t  ++ spc ()  ++ str"in "  ++ pr_id id)
+      (str"change "  ++ pr_constr t  ++ spc ()  ++ str"in "  ++ pr_id id)
 
   | Convert_hyp (id,Some c,t) ->
-      (str"change "  ++ print_constr8 c  ++ spc ()  ++ str"in "
+      (str"change "  ++ pr_constr c  ++ spc ()  ++ str"in "
        ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
       
   | Thin ids ->
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 4890b1bea2..f3cdfda47a 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -21,51 +21,76 @@ open Nametab
 open Termops
 open Evd
 open Proof_type
+open Rawterm
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
 
-val prterm_env      : env -> constr -> std_ppcmds
-val prterm_env_at_top : env -> constr -> std_ppcmds
-val prterm          : constr -> std_ppcmds
-val prtype_env      : env -> types -> std_ppcmds
-val prtype          : types -> std_ppcmds
-val prjudge_env     :
-  env -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
-val prjudge         : Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
-
-val pr_rawterm       : Rawterm.rawconstr -> std_ppcmds
-val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds
-
-val pr_constant     : env -> constant -> std_ppcmds
-val pr_existential  : env -> existential -> std_ppcmds
-val pr_constructor  : env -> constructor -> std_ppcmds
-val pr_inductive    : env -> inductive -> std_ppcmds
-val pr_global       : global_reference -> std_ppcmds
+(* Terms *)
+
+val pr_lconstr_env         : env -> constr -> std_ppcmds
+val pr_lconstr_env_at_top  : env -> constr -> std_ppcmds
+val pr_lconstr             : constr -> std_ppcmds
+
+val pr_constr_env          : env -> constr -> std_ppcmds
+val pr_constr              : constr -> std_ppcmds
+
+val pr_ltype_env           : env -> types -> std_ppcmds
+val pr_ltype               : types -> std_ppcmds
+
+val pr_type_env            : env -> types -> std_ppcmds
+val pr_type                : types -> std_ppcmds
+
+val pr_ljudge_env          : env -> unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge              : unsafe_judgment -> std_ppcmds * std_ppcmds
+
+val pr_lrawconstr_env      : env -> rawconstr -> std_ppcmds
+val pr_lrawconstr          : rawconstr -> std_ppcmds
+
+val pr_rawconstr_env       : env -> rawconstr -> std_ppcmds
+val pr_rawconstr           : rawconstr -> std_ppcmds
+
+val pr_constr_pattern_env  : env -> constr_pattern -> std_ppcmds
+val pr_constr_pattern      : constr_pattern -> std_ppcmds
+
+val pr_cases_pattern       : cases_pattern -> std_ppcmds
+
+(* Printing global references using names as short as possible *)
+
+val pr_global_env          : Idset.t -> global_reference -> std_ppcmds
+val pr_global              : global_reference -> std_ppcmds
+
+val pr_constant            : env -> constant -> std_ppcmds
+val pr_existential         : env -> existential -> std_ppcmds
+val pr_constructor         : env -> constructor -> std_ppcmds
+val pr_inductive           : env -> inductive -> std_ppcmds
 val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
-val pr_pattern      : constr_pattern -> std_ppcmds
-val pr_pattern_env  : env -> names_context -> constr_pattern -> std_ppcmds
 
-val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds
+(* Contexts *)
 
-val pr_var_decl     : env -> named_declaration -> std_ppcmds
-val pr_rel_decl     : env -> rel_declaration -> std_ppcmds
+val pr_ne_context_of       : std_ppcmds -> env -> std_ppcmds
 
-val pr_named_context : env -> named_context -> std_ppcmds
-val pr_named_context_of : env -> std_ppcmds
-val pr_rel_context  : env -> rel_context -> std_ppcmds
-val pr_rel_context_of  : env -> std_ppcmds
-val pr_context_of   : env -> std_ppcmds
+val pr_var_decl            : env -> named_declaration -> std_ppcmds
+val pr_rel_decl            : env -> rel_declaration -> std_ppcmds
 
-val emacs_str       : string -> string
+val pr_named_context       : env -> named_context -> std_ppcmds
+val pr_named_context_of    : env -> std_ppcmds
+val pr_rel_context         : env -> rel_context -> std_ppcmds
+val pr_rel_context_of      : env -> std_ppcmds
+val pr_context_of          : env -> std_ppcmds
 
 (* Proofs *)
-val pr_goal : goal -> std_ppcmds
-val pr_subgoals : evar_map -> goal list -> std_ppcmds
-val pr_subgoal   : int -> goal list -> std_ppcmds
 
-val pr_open_subgoals    : unit -> std_ppcmds
-val pr_nth_open_subgoal : int -> std_ppcmds
-val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds
+val pr_goal                : goal -> std_ppcmds
+val pr_subgoals            : evar_map -> goal list -> std_ppcmds
+val pr_subgoal             : int -> goal list -> std_ppcmds
 
-val pr_prim_rule : prim_rule -> std_ppcmds
+val pr_open_subgoals       : unit -> std_ppcmds
+val pr_nth_open_subgoal    : int -> std_ppcmds
+val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
+
+val pr_prim_rule           : prim_rule -> std_ppcmds
+
+(* Emacs/proof general support *)
+
+val emacs_str       : string -> string
diff --git a/parsing/search.ml b/parsing/search.ml
index 42b5cef5c2..580cb790c4 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -102,7 +102,7 @@ let constr_to_section_path c = match kind_of_term c with
 let xor a b = (a or b) & (not (a & b))
 
 let plain_display ref a c =
-  let pc = prterm_env a c in
+  let pc = pr_lconstr_env a c in
   let pr = pr_global ref in
   msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
 
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 827cfcd0e6..c003500533 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -70,7 +70,7 @@ let rec print_proof sigma osign pf =
 	  
 let pr_change gl = 
   str"Change " ++
-  prterm_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
+  pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
 
 let rec print_script nochange sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in