compat ocaml 3.03

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

11 files changed, 211 insertions, 211 deletions

diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
index 4663b3e37..63c176217 100644
--- a/contrib/correctness/pcicenv.ml
+++ b/contrib/correctness/pcicenv.ml
@@ -27,7 +27,7 @@ let modify_sign id t s =
   fold_named_context
     (fun ((x,b,ty) as d) sign ->
       if x=id then add_named_decl (x,b,t) sign else add_named_decl d sign)
-    s empty_named_context
+    s ~init:empty_named_context
 
 let add_sign (id,t) s =
   try 
diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml
index 1db31269b..c6e1636c6 100644
--- a/contrib/correctness/peffect.ml
+++ b/contrib/correctness/peffect.ml
@@ -143,17 +143,17 @@ open Util
 open Himsg
 
 let pp (r,w) =
-  hOV 0 [< if r<>[] then
-	     [< 'sTR"reads ";
-		prlist_with_sep (fun () -> [< 'sTR","; 'sPC >]) pr_id r >]
-	   else [< >];
-	   'sPC;
+  hov 0 (if r<>[] then
+	     (str"reads " ++
+		prlist_with_sep (fun () -> (str"," ++ spc ())) pr_id r)
+	   else (mt ()) ++
+	   spc () ++
 	   if w<>[] then
-	     [< 'sTR"writes ";
-		prlist_with_sep (fun ()-> [< 'sTR","; 'sPC >]) pr_id w >]
-	   else [< >]
-	>]
+	     (str"writes " ++
+		prlist_with_sep (fun ()-> (str"," ++ spc ())) pr_id w)
+	   else (mt ())
+)
 
 let ppr e =
-  pP (pp e)
+  Pp.pp (pp e)
 
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index c3cc1ec64..9ac7bee8e 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -223,7 +223,7 @@ let register id id' =
     let (v,p) = Idmap.find id !edited in
     let _ = add_global id' v (Some p) in
     Options.if_verbose 
-      mSGNL (hOV 0 [< 'sTR"Program "; pr_id id'; 'sPC; 'sTR"is defined" >]);
+      msgnl (hov 0 (str"Program " ++ pr_id id' ++ spc () ++ str"is defined"));
     edited := Idmap.remove id !edited
   with Not_found -> ()
 
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 17c673a54..19b4db992 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -30,38 +30,38 @@ let raise_with_loc = function
 let unbound_variable id loc =
   raise_with_loc loc
     (UserError ("Perror.unbound_variable",
-    (hOV 0 [<'sTR"Unbound variable"; 'sPC; pr_id id; 'fNL >])))
+    (hov 0 (str"Unbound variable" ++ spc () ++ pr_id id ++ fnl ()))))
 
 let unbound_reference id loc =
   raise_with_loc loc
     (UserError ("Perror.unbound_reference",
-    (hOV 0 [<'sTR"Unbound reference"; 'sPC; pr_id id; 'fNL >])))
+    (hov 0 (str"Unbound reference" ++ spc () ++ pr_id id ++ fnl ()))))
 
 let clash id loc =
   raise_with_loc loc
     (UserError ("Perror.clash",
-    (hOV 0 [< 'sTR"Clash with previous constant"; 'sPC;
-    'sTR(string_of_id id); 'fNL >])))
+    (hov 0 (str"Clash with previous constant" ++ spc () ++
+    str(string_of_id id) ++ fnl ()))))
 
 let not_defined id =
   raise
     (UserError ("Perror.not_defined",
-	       	(hOV 0 [< 'sTR"The object"; 'sPC; pr_id id; 'sPC;
-			  'sTR"is not defined"; 'fNL >])))
+	       	(hov 0 (str"The object" ++ spc () ++ pr_id id ++ spc () ++
+			  str"is not defined" ++ fnl ()))))
 
 let check_for_reference loc id = function
     Ref _ -> ()
   | _ -> Stdpp.raise_with_loc loc 
 	(UserError ("Perror.check_for_reference",
-		    hOV 0 [< pr_id id; 'sPC; 
-			     'sTR"is not a reference" >]))
+		    hov 0 (pr_id id ++ spc () ++ 
+			     str"is not a reference")))
 
 let check_for_array loc id = function
     Array _ -> ()
   | _ -> Stdpp.raise_with_loc loc 
 	(UserError ("Perror.check_for_array",
-		    hOV 0 [< pr_id id; 'sPC; 
-			     'sTR"is not an array" >]))
+		    hov 0 (pr_id id ++ spc () ++ 
+			     str"is not an array")))
 
 let is_constant_type s = function
     TypePure c ->
@@ -75,56 +75,56 @@ let check_for_index_type loc v =
   if not is_index then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_index",
-		  hOV 0 [< 'sTR"This expression is an index"; 'sPC; 
-			   'sTR"and should have type int (Z)" >]))
+		  hov 0 (str"This expression is an index" ++ spc () ++ 
+			   str"and should have type int (Z)")))
 
 let check_no_effect loc ef =
   if not (Peffect.get_writes ef = []) then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_no_effect",
-		  hOV 0 [< 'sTR"A boolean should not have side effects"
-		        >]))
+		  hov 0 (str"A boolean should not have side effects"
+)))
 
 let should_be_boolean loc =
   Stdpp.raise_with_loc loc 
     (UserError ("Perror.should_be_boolean",
-		hOV 0 [< 'sTR"This expression is a test:" ; 'sPC;
-			 'sTR"it should have type bool" >]))
+		hov 0 (str"This expression is a test:" ++ spc () ++
+			 str"it should have type bool")))
 
 let test_should_be_annotated loc =
   Stdpp.raise_with_loc loc 
     (UserError ("Perror.test_should_be_annotated",
-		hOV 0 [< 'sTR"This test should be annotated" >]))
+		hov 0 (str"This test should be annotated")))
 
 let if_branches loc =
   Stdpp.raise_with_loc loc 
     (UserError ("Perror.if_branches",
-		hOV 0 [< 'sTR"The two branches of an `if' expression" ; 'sPC;
-			 'sTR"should have the same type" >]))
+		hov 0 (str"The two branches of an `if' expression" ++ spc () ++
+			 str"should have the same type")))
 
 let check_for_not_mutable loc v =
   if is_mutable v then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_not_mutable",
-		  hOV 0 [< 'sTR"This expression cannot be a mutable" >]))
+		  hov 0 (str"This expression cannot be a mutable")))
 
 let check_for_pure_type loc v =
   if not (is_pure v) then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_pure_type",
-		  hOV 0 [< 'sTR"This expression must be pure"; 'sPC;
-			   'sTR"(neither a mutable nor a function)" >]))
+		  hov 0 (str"This expression must be pure" ++ spc () ++
+			   str"(neither a mutable nor a function)")))
 
 let check_for_let_ref loc v =
   if not (is_pure v) then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_let_ref",
-		  hOV 0 [< 'sTR"References can only be bound in pure terms">]))
+		  hov 0 (str"References can only be bound in pure terms")))
 
 let informative loc s =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.variant_informative",
-	      hOV 0 [< 'sTR s; 'sPC; 'sTR"must be informative" >]))
+	      hov 0 (str s ++ spc () ++ str"must be informative")))
 
 let variant_informative loc = informative loc "Variant"
 let should_be_informative loc = informative loc "This term"
@@ -132,41 +132,41 @@ let should_be_informative loc = informative loc "This term"
 let app_of_non_function loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.app_of_non_function",
-	      hOV 0 [< 'sTR"This term cannot be applied"; 'sPC;
-		       'sTR"(either it is not a function"; 'sPC;
-		       'sTR"or it is applied to non pure arguments)" >]))
+	      hov 0 (str"This term cannot be applied" ++ spc () ++
+		       str"(either it is not a function" ++ spc () ++
+		       str"or it is applied to non pure arguments)")))
   
 let partial_app loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.partial_app",
-	      hOV 0 [< 'sTR"This function does not have";
-		       'sPC; 'sTR"the right number of arguments" >]))
+	      hov 0 (str"This function does not have" ++
+		       spc () ++ str"the right number of arguments")))
   
 let expected_type loc s =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.expected_type",
-	      hOV 0 [< 'sTR"Argument is expected to have type"; 'sPC; s >]))
+	      hov 0 (str"Argument is expected to have type" ++ spc () ++ s)))
 
 let expects_a_type id loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.expects_a_type",
-	      hOV 0 [< 'sTR"The argument "; pr_id id; 'sPC;
-		       'sTR"in this application is supposed to be a type" >]))
+	      hov 0 (str"The argument " ++ pr_id id ++ spc () ++
+		       str"in this application is supposed to be a type")))
 
 let expects_a_term id =
   raise
   (UserError ("Perror.expects_a_type",
-	      hOV 0 [< 'sTR"The argument "; pr_id id; 'sPC;
-		       'sTR"in this application is supposed to be a term" >]))
+	      hov 0 (str"The argument " ++ pr_id id ++ spc () ++
+		       str"in this application is supposed to be a term")))
 
 let should_be_a_variable loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.should_be_a_variable",
-	      hOV 0 [< 'sTR"Argument should be a variable" >]))
+	      hov 0 (str"Argument should be a variable")))
    
 let should_be_a_reference loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.should_be_a_reference",
-	      hOV 0 [< 'sTR"Argument of function should be a reference" >]))
+	      hov 0 (str"Argument of function should be a reference")))
 
    
diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
index a097ac1b5..47fc9929f 100644
--- a/contrib/correctness/pextract.ml
+++ b/contrib/correctness/pextract.ml
@@ -42,18 +42,18 @@ let access = ConstRef sp_access
 let has_array = ref false
 
 let pp_conversions () =
-  [< 'sTR"\
+  (str"\
 let rec int_of_pos = function
     XH -> 1
   | XI p -> 2 * (int_of_pos p) + 1
   | XO p -> 2 * (int_of_pos p)
-;;
+ ++ ++
 
 let int_of_z = function
     ZERO -> 0
   | POS p -> int_of_pos p
   | NEG p -> -(int_of_pos p)
-;;
+ ++ ++
 " >] (* '"' *)
 
 (* collect all section-path in a CIC constant *)
@@ -61,7 +61,7 @@ let int_of_z = function
 let spset_of_cci env c =
   let spl = Fw_env.collect (extraction env c) in
   let sps = List.fold_left (fun e x -> SpSet.add x e) SpSet.empty spl in
-  has_array := !has_array or (SpSet.mem sp_access sps);
+  has_array := !has_array or (SpSet.mem sp_access sps) ++
   SpSet.remove sp_access sps
 
 
@@ -81,10 +81,10 @@ let collect env =
     | Acc x -> add_id env s x
     | Aff (x,e1) -> add_id env (collect_rec env s e1) x
     | TabAcc (_,x,e1) ->
-	has_array := true;
+	has_array := true ++
 	add_id env (collect_rec env s e1) x
     | TabAff (_,x,e1,e2) ->
-	has_array := true;
+	has_array := true ++
 	add_id env (collect_rec env (collect_rec env s e1) e2) x
     | Seq bl ->
 	List.fold_left (fun s st -> match st with
@@ -144,17 +144,17 @@ module Ocaml_ren = Ocaml.OCaml_renaming
 
 let rename_global id =
   let id' = Ocaml_ren.rename_global_term !Fwtoml.globals (Name id) in
-  Fwtoml.add_global_renaming (id,id');
+  Fwtoml.add_global_renaming (id,id') ++
   id'
 
-type rename_struct = { rn_map : identifier IdMap.t;
+type rename_struct = { rn_map : identifier IdMap.t ++
 		       rn_avoid : identifier list }
 
-let rn_empty = { rn_map = IdMap.empty; rn_avoid = [] }
+let rn_empty = { rn_map = IdMap.empty ++ rn_avoid = [] }
 
 let rename_local rn id =
   let id' = Ocaml_ren.rename_term (!Fwtoml.globals@rn.rn_avoid) (Name id) in
-  { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid },
+  { rn_map = IdMap.add id id' rn.rn_map ++ rn_avoid = id' :: rn.rn_avoid },
   id'
 
 let get_local_name rn id = IdMap.find id rn.rn_map
@@ -177,7 +177,7 @@ let rec rename_binders rn = function
  *)
 
 let putpar par s =
-  if par then [< 'sTR"("; s; 'sTR")" >] else s
+  if par then (str"(" ++ s ++ str")") else s
 
 let is_ref env id =
   try
@@ -188,21 +188,21 @@ let is_ref env id =
 let rec pp_constr env rn = function
   | VAR id ->
       if is_ref env id then 
-	[< 'sTR"!"; pID (get_name env rn id) >] 
+	(str"!" ++ pID (get_name env rn id)) 
       else
 	pID (get_name env rn id)
   | DOPN((Const _|MutInd _|MutConstruct _) as oper, _) ->
       pID (Fwtoml.name_of_oper oper)
   | DOPN(AppL,v) ->
       if Array.length v = 0 then
-	  [< >]
+	  (mt ())
       else begin
 	match v.(0) with
 	    DOPN(Const sp,_) when sp = sp_access ->
-	      [< pp_constr env rn v.(3); 
-		 'sTR".(int_of_z "; pp_constr env rn v.(4); 'sTR")" >]
+	      (pp_constr env rn v.(3) ++ 
+		 str".(int_of_z " ++ pp_constr env rn v.(4) ++ str")")
 	  | _ ->
-	      hOV 2 (putpar true (prvect_with_sep (fun () -> [< 'sPC >])
+	      hov 2 (putpar true (prvect_with_sep (fun () -> (spc ()))
 				    (pp_constr env rn) v))
       end
   | DOP2(Cast,c,_) -> pp_constr env rn c
@@ -219,95 +219,95 @@ let collect_lambda =
   collect []
 
 let pr_binding rn = 
-  prlist_with_sep (fun () -> [< >])
+  prlist_with_sep (fun () -> (mt ()))
     (function 
        | (id,(Untyped | BindType _)) -> 
-	   [< 'sTR" "; pID (get_local_name rn id) >]
-       | (id,BindSet) -> [< >])
+	   (str" " ++ pID (get_local_name rn id))
+       | (id,BindSet) -> (mt ()))
 
 let pp_prog id =
   let rec pp_d env rn par = function
     | Var x -> pID (get_name env rn x)
-    | Acc x -> [< 'sTR"!"; pID (get_name env rn x) >]
-    | Aff (x,e1) -> [< pID (get_name env rn x); 
-		       'sTR" := "; hOV 0 (pp env rn false e1) >]
+    | Acc x -> (str"!" ++ pID (get_name env rn x))
+    | Aff (x,e1) -> (pID (get_name env rn x) ++ 
+		       str" := " ++ hov 0 (pp env rn false e1))
     | TabAcc (_,x,e1) ->
-	[< pID (get_name env rn x); 
-	   'sTR".(int_of_z "; hOV 0 (pp env rn true e1); 'sTR")" >]
+	(pID (get_name env rn x) ++ 
+	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")")
     | TabAff (_,x,e1,e2) ->
-	[< pID (get_name env rn x);
-	   'sTR".(int_of_z "; hOV 0 (pp env rn true e1); 'sTR")";
-	   'sTR" <-"; 'sPC; hOV 2 (pp env rn false e2) >]
+	(pID (get_name env rn x) ++
+	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")" ++
+	   str" <-" ++ spc () ++ hov 2 (pp env rn false e2))
     | Seq bl ->
-	[< 'sTR"begin"; 'fNL;
-	   'sTR"  "; hOV 0 [< pp_block env rn bl; >]; 'fNL;
-	   'sTR"end" >]
+	(str"begin" ++ fnl () ++
+	   str"  " ++ hov 0 (pp_block env rn bl ++) ++ fnl () ++
+	   str"end")
     | If (e1,e2,e3) ->
-	putpar par [< 'sTR"if "; (pp env rn false e1);
-		      'sTR" then"; 'fNL;
-		      'sTR"  "; hOV 0 (pp env rn false e2); 'fNL;
-		      'sTR"else"; 'fNL;
-		      'sTR"  "; hOV 0 (pp env rn false e3) >]
+	putpar par (str"if " ++ (pp env rn false e1) ++
+		      str" then" ++ fnl () ++
+		      str"  " ++ hov 0 (pp env rn false e2) ++ fnl () ++
+		      str"else" ++ fnl () ++
+		      str"  " ++ hov 0 (pp env rn false e3))
 	(* optimisations : then begin .... end else begin ... end *)
     | While (b,inv,_,bl) ->
-	[< 'sTR"while "; (pp env rn false b); 'sTR" do"; 'fNL;		    
-	   'sTR"  ";
-	   hOV 0 [< (match inv with
-			 None -> [< >] 
-		       | Some c -> [< 'sTR"(* invariant: "; pTERM c.a_value ; 
-				      'sTR" *)"; 'fNL >]);
-		    pp_block env rn bl; >]; 'fNL;
-	   'sTR"done"; >]
+	(str"while " ++ (pp env rn false b) ++ str" do" ++ fnl () ++		    
+	   str"  " ++
+	   hov 0 ((match inv with
+			 None -> (mt ()) 
+		       | Some c -> (str"(* invariant: " ++ pTERM c.a_value ++ 
+				      str" *)" ++ fnl ())) ++
+		    pp_block env rn bl ++) ++ fnl () ++
+	   str"done" ++)
     | Lam (bl,e) ->
 	let env' = traverse_binders env bl in
 	let rn' = rename_binders rn bl in
 	  putpar par 
-	    (hOV 2 [< 'sTR"fun"; pr_binding rn' bl; 'sTR" ->";
-		      'sPC; pp env' rn' false e >])
-    | SApp ((Var id)::_,  [e1; e2])
+	    (hov 2 (str"fun" ++ pr_binding rn' bl ++ str" ->" ++
+		      spc () ++ pp env' rn' false e))
+    | SApp ((Var id)::_,  [e1 ++ e2])
 	when id = connective_and or id = connective_or ->
 	  let conn = if id = connective_and then "&" else "or" in
 	  putpar par 
-	    (hOV 0 [< pp env rn true e1; 'sPC; 'sTR conn; 'sPC;
-		      pp env rn true e2 >])
+	    (hov 0 (pp env rn true e1 ++ spc () ++ str conn ++ spc () ++
+		      pp env rn true e2))
     | SApp ((Var id)::_, [e]) when id = connective_not ->
 	putpar par 
-	  (hOV 0 [< 'sTR"not"; 'sPC; pp env rn true e >])
+	  (hov 0 (str"not" ++ spc () ++ pp env rn true e))
     | SApp _ ->
 	invalid_arg "Prog_extract.pp_prog (SApp)"
     | App(e1,[]) ->
-	hOV 0 (pp env rn false e1)
+	hov 0 (pp env rn false e1)
     | App (e1,l) ->
 	putpar true
-	  (hOV 2 [< pp env rn true e1;
+	  (hov 2 (pp env rn true e1 ++
 		    prlist (function 
-				Term p -> [< 'sPC; pp env rn true p >]
-			      | Refarg x -> [< 'sPC; pID (get_name env rn x) >]
-			      | Type _ -> [< >]) 
-		      l >])
+				Term p -> (spc () ++ pp env rn true p)
+			      | Refarg x -> (spc () ++ pID (get_name env rn x))
+			      | Type _ -> (mt ())) 
+		      l))
     | LetRef (x,e1,e2) ->
 	let (_,v),_,_,_ = e1.info.kappa in
 	let env' = add (x,Ref v) env in
 	let rn',x' = rename_local rn x in
 	putpar par 
-	  (hOV 0 [< 'sTR"let "; pID x'; 'sTR" = ref "; pp env rn false e1;
-		    'sTR" in"; 'fNL; pp env' rn' false e2 >])
+	  (hov 0 (str"let " ++ pID x' ++ str" = ref " ++ pp env rn false e1 ++
+		    str" in" ++ fnl () ++ pp env' rn' false e2))
     | LetIn (x,e1,e2) ->
 	let (_,v),_,_,_ = e1.info.kappa in
 	let env' = add (x,v) env in
 	let rn',x' = rename_local rn x in
 	putpar par 
-	  (hOV 0 [< 'sTR"let "; pID x'; 'sTR" = "; pp env rn false e1;
-		    'sTR" in"; 'fNL; pp env' rn' false e2 >])
+	  (hov 0 (str"let " ++ pID x' ++ str" = " ++ pp env rn false e1 ++
+		    str" in" ++ fnl () ++ pp env' rn' false e2))
     | LetRec (f,bl,_,_,e) ->
 	let env' = traverse_binders env bl in
 	let rn' = rename_binders rn bl in
 	let env'' = add (f,make_arrow bl e.info.kappa) env' in
 	let rn'',f' = rename_local rn' f in
 	putpar par 
-	  (hOV 0 [< 'sTR"let rec "; pID f'; pr_binding rn' bl; 'sTR" ="; 'fNL;
-		    'sTR"  "; hOV 0 [< pp env'' rn'' false e >]; 'fNL;
-		    'sTR"in "; pID f' >])
+	  (hov 0 (str"let rec " ++ pID f' ++ pr_binding rn' bl ++ str" =" ++ fnl () ++
+		    str"  " ++ hov 0 (pp env'' rn'' false e) ++ fnl () ++
+		    str"in " ++ pID f'))
     | Debug (_,e1) -> pp env rn par e1
     | PPoint (_,d) -> pp_d env rn par d
     | Expression c -> 
@@ -317,21 +317,21 @@ let pp_prog id =
     let bl =
       map_succeed (function Statement p -> p | _ -> failwith "caught") bl
     in
-      prlist_with_sep (fun () -> [< 'sTR";"; 'fNL >])
-      	(fun p -> hOV 0 (pp env rn false p)) bl
+      prlist_with_sep (fun () -> (str";" ++ fnl ()))
+      	(fun p -> hov 0 (pp env rn false p)) bl
 
   and pp env rn par p = 
-    [< pp_d env rn par p.desc >]
+    (pp_d env rn par p.desc)
 
   and pp_mut v c = match v with
     | Ref _ ->
-	[< 'sTR"ref "; pp_constr empty rn_empty (extraction empty c) >]
+	(str"ref " ++ pp_constr empty rn_empty (extraction empty c))
     | Array (n,_) ->
-	[< 'sTR"Array.create "; 'cUT;
+	(str"Array.create " ++ cut () ++
 	   putpar true 
-	     [< 'sTR"int_of_z ";
-		pp_constr empty rn_empty (extraction empty n) >];
-	   'sTR" "; pp_constr empty rn_empty (extraction empty c) >]
+	     (str"int_of_z " ++
+		pp_constr empty rn_empty (extraction empty n)) ++
+	   str" " ++ pp_constr empty rn_empty (extraction empty c))
     | _ -> invalid_arg "pp_mut"
   in
   let v = lookup_global id in
@@ -339,23 +339,23 @@ let pp_prog id =
     if is_mutable v then
       try
 	let c = find_init id in
-	hOV 0 [< 'sTR"let "; pID id'; 'sTR" = "; pp_mut v c >]
+	hov 0 (str"let " ++ pID id' ++ str" = " ++ pp_mut v c)
       with Not_found -> 
 	errorlabstrm "Prog_extract.pp_prog"
-	  [< 'sTR"The variable "; pID id;
-	     'sTR" must be initialized first !" >]
+	  (str"The variable " ++ pID id ++
+	     str" must be initialized first !")
     else
       match find_pgm id with
 	| None -> 
 	    errorlabstrm "Prog_extract.pp_prog"
-	      [< 'sTR"The program "; pID id;
-		 'sTR" must be realized first !" >]
+	      (str"The program " ++ pID id ++
+		 str" must be realized first !")
       	| Some p ->
 	    let bl,p = collect_lambda p in
 	    let rn = rename_binders rn_empty bl in
 	    let env = traverse_binders empty bl in
-	    hOV 0  [< 'sTR"let "; pID id'; pr_binding rn bl; 'sTR" ="; 'fNL; 
-		      'sTR"  "; hOV 2 (pp env rn false p) >]
+	    hov 0  (str"let " ++ pID id' ++ pr_binding rn bl ++ str" =" ++ fnl () ++ 
+		      str"  " ++ hov 2 (pp env rn false p))
 
 (* extraction des programmes impératifs/fonctionnels vers ocaml *)
 
@@ -375,7 +375,7 @@ let import sp = match repr_path sp with
   | _ -> ()
 
 let pp_ocaml file prm =
-  has_array := false;
+  has_array := false ++
   (* on separe objects Coq et programmes *)
   let cic,pgms =
     List.fold_left
@@ -404,7 +404,7 @@ let pp_ocaml file prm =
 	   in
 	   let cic' = 
 	     SpSet.fold 
-	       (fun sp cic -> import sp; IdSet.add (basename sp) cic)
+	       (fun sp cic -> import sp ++ IdSet.add (basename sp) cic)
 	       spl cic
 	   in
 	   (cic',IdSet.union pgms pgms',id::pl)
@@ -414,23 +414,23 @@ let pp_ocaml file prm =
   in
   let cic = IdSet.elements cic in
   (* on pretty-print *)
-  let prm' = { needed = cic; expand = prm.expand; 
-	       expansion = prm.expansion; exact = prm.exact } 
+  let prm' = { needed = cic ++ expand = prm.expand ++ 
+	       expansion = prm.expansion ++ exact = prm.exact } 
   in
-  let strm = [< Ocaml.OCaml_pp_file.pp_recursive prm';
-		'fNL; 'fNL;
-		if !has_array then pp_conversions() else [< >];
-		prlist (fun p -> [< pp_prog p; 'fNL; 'sTR";;"; 'fNL; 'fNL >])
+  let strm = (Ocaml.OCaml_pp_file.pp_recursive prm' ++
+		fnl () ++ fnl () ++
+		if !has_array then pp_conversions() else (mt ()) ++
+		prlist (fun p -> (pp_prog p ++ fnl () ++ str";;" ++ fnl () ++ fnl ()))
 		  pgms
-	     >]
+)
   in
   (* puis on ecrit dans le fichier *)
   let chan = open_trapping_failure open_out file ".ml" in
   let ft = with_output_to chan in
   begin
-    try  pP_with ft strm ; pp_flush_with ft ()
-    with e -> pp_flush_with ft () ; close_out chan; raise e
-  end;
+    try  pP_with ft strm ++ pp_flush_with ft ()
+    with e -> pp_flush_with ft () ++ close_out chan ++ raise e
+  end ++
   close_out chan
     
 
@@ -450,10 +450,10 @@ let initialize id com =
       initialize id c
     else
       errorlabstrm "Prog_extract.initialize"
-	[< 'sTR"Not the expected type for the mutable "; pID id >]
+	(str"Not the expected type for the mutable " ++ pID id)
   with Not_found -> 
     errorlabstrm "Prog_extract.initialize"
-      [< pr_id id; 'sTR" is not a mutable" >]
+      (pr_id id ++ str" is not a mutable")
 
 (* grammaire *)
 
@@ -467,6 +467,6 @@ let _ = vinterp_add "IMPERATIVEEXTRACTION"
 	  
 let _ = vinterp_add "INITIALIZE"
 	  (function 
-	     | [VARG_IDENTIFIER id ; VARG_COMMAND com] ->
+	     | [VARG_IDENTIFIER id ++ VARG_COMMAND com] ->
 		 (fun () -> initialize id com)
 	     | _ -> assert false)
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6d04befe2..36e4f0dc9 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -22,7 +22,7 @@ let debug = ref false
 
 let deb_mess s =
   if !debug then begin
-    mSGNL s;  pp_flush()
+    msgnl s;  pp_flush()
   end
 
 let list_of_some = function
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml
index 122ff16ab..aa068f19c 100644
--- a/contrib/correctness/prename.ml
+++ b/contrib/correctness/prename.ml
@@ -111,8 +111,8 @@ let var_at_date r d id =
     find (until d r) id
   with Not_found ->
     raise (UserError ("Renamings.var_at_date",
-	      hOV 0 [< 'sTR"Variable "; pr_id id; 'sTR" is unknown"; 'sPC;
-		       'sTR"at date "; 'sTR d >]))
+	      hov 0 (str"Variable " ++ pr_id id ++ str" is unknown" ++ spc () ++
+		       str"at date " ++ str d)))
 
 let vars_at_date r d ids =
   let r' = until d r in List.map (fun id -> id,find r' id) ids
@@ -125,15 +125,15 @@ open Util
 open Himsg
 
 let pp r = 
-  hOV 2 (prlist_with_sep (fun () -> [< 'fNL >])
+  hov 2 (prlist_with_sep (fun () -> (fnl ()))
 	   (fun (d,l) -> 
-	      [< 'sTR d; 'sTR": "; 
-		 prlist_with_sep (fun () -> [< 'sPC >])
+	      (str d ++ str": " ++ 
+		 prlist_with_sep (fun () -> (spc ()))
 		   (fun (id,id') -> 
-		      [< 'sTR"("; pr_id id; 'sTR","; pr_id id'; 'sTR")" >])
-		   l >])
+		      (str"(" ++ pr_id id ++ str"," ++ pr_id id' ++ str")"))
+		   l))
 	   r.levels)
 
 let ppr e =
-  pP (pp e)
+  Pp.pp (pp e)
 
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 6b487348a..361791414 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -490,12 +490,12 @@ open Declare
 
 let is_assumed global ids =
   if List.length ids = 1 then
-    mSGNL [< 'sTR (if global then "A global variable " else ""); 
-	     pr_id (List.hd ids); 'sTR " is assumed" >]
+    msgnl (str (if global then "A global variable " else "") ++ 
+	     pr_id (List.hd ids) ++ str " is assumed")
   else
-    mSGNL [< 'sTR (if global then "Some global variables " else "");
-	     prlist_with_sep (fun () -> [< 'sTR ", " >]) pr_id ids;
-	     'sTR " are assumed" >]
+    msgnl (str (if global then "Some global variables " else "") ++
+	     prlist_with_sep (fun () -> (str ", ")) pr_id ids ++
+	     str " are assumed")
 
 let add = vinterp_add
 
@@ -521,10 +521,10 @@ let _ =
 	   (fun () ->
 	      fold_all 
 		(fun (id,v) _ -> 
-		   mSGNL [< pr_id id; 'sTR " : "; 
-			    hOV 2 (match v with TypeV v -> pp_type_v v
-				     | Set -> [< 'sTR "Set" >]);
-			    'fNL >])
+		   msgnl (pr_id id ++ str " : " ++ 
+			    hov 2 (match v with TypeV v -> pp_type_v v
+				     | Set -> (str "Set")) ++
+			    fnl ()))
 		Penv.empty ())
        | _ -> assert false)
 
@@ -539,7 +539,7 @@ let _ =
 	      List.iter
 		(fun id -> if Penv.is_global id then
 		   Util.errorlabstrm "PROGVARIABLE"
-		     [< 'sTR"Clash with previous constant "; pr_id id >])
+		     (str"Clash with previous constant " ++ pr_id id))
 		ids;
 	      let v = out_typev d in
 	      Pdb.check_type_v (all_refs ()) v;
@@ -575,13 +575,13 @@ GEXTEND Gram
 
     | IDENT "Correctness"; s = IDENT; p = Programs.program; "." ->
 	let d = Ast.dynamic (in_prog p) in
-	let str = Ast.str s in
+	let str = Ast.string s in
 	<:ast< (CORRECTNESS $str (VERNACDYN $d)) >>
 
     | IDENT "Correctness"; s = IDENT; p = Programs.program; ";";
       tac = Tactic.tactic; "." ->
 	let d = Ast.dynamic (in_prog p) in
-	let str = Ast.str s in
+	let str = Ast.string s in
 	<:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> ] ];
   Pcoq.Vernac_.command:
   [ [ IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >>
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 011c3c7e8..e8f10fc89 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -37,7 +37,7 @@ let coqast_of_prog p =
   let p = Pdb.db_prog p in
 
   (* 2. typage avec effets *)
-  deb_mess [< 'sTR"Ptyping.states: Typing with effects..."; 'fNL >];
+  deb_mess (str"Ptyping.states: Typing with effects..." ++ fnl ());
   let env = Penv.empty in
   let ren = initial_renaming env in
   let p = Ptyping.states ren env p in
@@ -54,20 +54,20 @@ let coqast_of_prog p =
 
   (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
   deb_mess 
-    [< 'fNL; 'sTR"Mlize.trad: Translation program -> cc_term..."; 'fNL >];
+    (fnl () ++ str"Mlize.trad: Translation program -> cc_term..." ++ fnl ());
   let cc = Pmlize.trans ren p in
   let cc = Pred.red cc in
   deb_mess (Putil.pp_cc_term cc);
 
   (* 5. traduction en constr *)
   deb_mess 
-    [< 'fNL; 'sTR"Pcic.constr_of_prog: Translation cc_term -> rawconstr..."; 
-       'fNL >];
+    (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ 
+       fnl ());
   let r = Pcic.rawconstr_of_prog cc in
   deb_mess (Printer.pr_rawterm r);
 
   (* 6. résolution implicites *)
-  deb_mess [< 'fNL; 'sTR"Resolution implicits (? => Meta(n))..."; 'fNL >];
+  deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ());
   let oc = understand_gen_tcc Evd.empty (Global.env()) [] [] None r in
   deb_mess (Printer.prterm (snd oc));
 
@@ -227,9 +227,9 @@ let correctness s p opttac =
   start_proof id Declare.NeverDischarge sign cty;
   Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
-  deb_mess [< 'sTR"Pred.red_cci: Reduction..."; 'fNL >];
+  deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
   let oc = reduce_open_constr oc in
-  deb_mess [< 'sTR"AFTER REDUCTION:"; 'fNL >];
+  deb_mess (str"AFTER REDUCTION:" ++ fnl ());
   deb_mess (Printer.prterm (snd oc));
   let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
   let tac = match opttac with 
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index 2e95f840f..a6f7a0ae9 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -529,7 +529,7 @@ let rec states_desc ren env loc = function
 	if s_e.info.kappa = c then
 	  s_e
       	else begin
-	  if !verbose_fix then begin mSGNL (pp_type_c s_e.info.kappa) end ;
+	  if !verbose_fix then begin msgnl (pp_type_c s_e.info.kappa) end ;
 	  state_rec s_e.info.kappa
       	end
       in 
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 5e454a252..dbb903ab1 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -235,70 +235,70 @@ open Util
 open Printer
 
 let pp_pre = function
-    [] -> [< >]
+    [] -> (mt ())
   | l  ->
-      hOV 0 [< 'sTR"pre "; 
-	       prlist_with_sep (fun () -> [< 'sPC >]) 
-		 (fun x -> prterm x.p_value) l >]
+      hov 0 (str"pre " ++ 
+	       prlist_with_sep (fun () -> (spc ())) 
+		 (fun x -> prterm x.p_value) l)
 
 let pp_post = function
-    None -> [< >]
-  | Some c -> hOV 0 [< 'sTR"post "; prterm c.a_value >]
+    None -> (mt ())
+  | Some c -> hov 0 (str"post " ++ prterm c.a_value)
 
 let rec pp_type_v = function
-    Ref v -> hOV 0 [< pp_type_v v; 'sPC; 'sTR"ref" >]
-  | Array (cc,v) -> hOV 0 [< 'sTR"array "; prterm cc; 'sTR" of "; pp_type_v v >]
+    Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref")
+  | Array (cc,v) -> hov 0 (str"array " ++ prterm cc ++ str" of " ++ pp_type_v v)
   | Arrow (b,c) -> 
-      hOV 0 [< prlist_with_sep (fun () -> [< >]) pp_binder b; 
-	       pp_type_c c >]
+      hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++ 
+	       pp_type_c c)
   | TypePure c -> prterm c
 
 and pp_type_c ((id,v),e,p,q) =
-  hOV 0 [< 'sTR"returns "; pr_id id; 'sTR":"; pp_type_v v; 'sPC; 
-	   Peffect.pp e; 'sPC; pp_pre p; 'sPC; pp_post q ;
-	   'sPC; 'sTR"end" >]
+  hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++ 
+	   Peffect.pp e ++ spc () ++ pp_pre p ++ spc () ++ pp_post q ++
+	   spc () ++ str"end")
 
 and pp_binder = function
-    id,BindType v -> [< 'sTR"("; pr_id id; 'sTR":"; pp_type_v v; 'sTR")" >]
-  | id,BindSet -> [< 'sTR"("; pr_id id; 'sTR":Set)" >]
-  | id,Untyped -> [< 'sTR"("; pr_id id; 'sTR")" >]
+    id,BindType v -> (str"(" ++ pr_id id ++ str":" ++ pp_type_v v ++ str")")
+  | id,BindSet -> (str"(" ++ pr_id id ++ str":Set)")
+  | id,Untyped -> (str"(" ++ pr_id id ++ str")")
 
 (* pretty-print of cc-terms (intermediate terms) *)
 
 let rec pp_cc_term = function
     CC_var id -> pr_id id
   | CC_letin (_,_,bl,c,c1) ->
-      hOV 0 [< hOV 2 [< 'sTR"let ";
-		  	prlist_with_sep (fun () -> [< 'sTR"," >])
-			  (fun (id,_) -> pr_id id) bl;
-		  	'sTR" ="; 'sPC;
-		  	pp_cc_term c;
-		  	'sTR " in">];
-	       'fNL;
-	       pp_cc_term c1 >]
+      hov 0 (hov 2 (str"let " ++
+		  	prlist_with_sep (fun () -> (str","))
+			  (fun (id,_) -> pr_id id) bl ++
+		  	str" =" ++ spc () ++
+		  	pp_cc_term c ++
+		  	str " in") ++
+	       fnl () ++
+	       pp_cc_term c1)
   | CC_lam (bl,c) ->
-      hOV 2 [< prlist (fun (id,_) -> [< 'sTR"["; pr_id id; 'sTR"]" >]) bl;
-	       'cUT;
-	       pp_cc_term c >]
+      hov 2 (prlist (fun (id,_) -> (str"[" ++ pr_id id ++ str"]")) bl ++
+	       cut () ++
+	       pp_cc_term c)
   | CC_app (f,args) ->
-      hOV 2 [< 'sTR"("; 
-	       pp_cc_term f; 'sPC;
-	       prlist_with_sep (fun () -> [< 'sPC >]) pp_cc_term args;
-	       'sTR")" >]
+      hov 2 (str"(" ++ 
+	       pp_cc_term f ++ spc () ++
+	       prlist_with_sep (fun () -> (spc ())) pp_cc_term args ++
+	       str")")
   | CC_tuple (_,_,cl) ->
-      hOV 2 [< 'sTR"(";
-	       prlist_with_sep (fun () -> [< 'sTR","; 'cUT >])
-		 pp_cc_term cl;
-	       'sTR")" >]
+      hov 2 (str"(" ++
+	       prlist_with_sep (fun () -> (str"," ++ cut ()))
+		 pp_cc_term cl ++
+	       str")")
   | CC_case (_,b,[e1;e2]) ->
-      hOV 0 [< 'sTR"if "; pp_cc_term b; 'sTR" then"; 'fNL;
-	       'sTR"  "; hOV 0 (pp_cc_term e1); 'fNL;
-	       'sTR"else"; 'fNL;
-	       'sTR"  "; hOV 0 (pp_cc_term e2) >]
+      hov 0 (str"if " ++ pp_cc_term b ++ str" then" ++ fnl () ++
+	       str"  " ++ hov 0 (pp_cc_term e1) ++ fnl () ++
+	       str"else" ++ fnl () ++
+	       str"  " ++ hov 0 (pp_cc_term e2))
   | CC_case _ ->
-      hOV 0 [< 'sTR"<Case: not yet implemented>" >]
+      hov 0 (str"<Case: not yet implemented>")
   | CC_expr c ->
-      hOV 0 (prterm c)
+      hov 0 (prterm c)
   | CC_hole c ->
-      [< 'sTR"(?::"; prterm c; 'sTR")" >]
+      (str"(?::" ++ prterm c ++ str")")