compat ocaml 3.03

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

8 files changed, 179 insertions, 171 deletions

diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index eae99993f..00db51adf 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -54,11 +54,11 @@ set_flags := (function () ->
                   (g_nat_syntax_flag := true; ())
                 else ());;
 
-let guarded_force_eval_stream s = 
+let guarded_force_eval_stream (s : std_ppcmds) = 
   let l = ref [] in
   let f elt = l:= elt :: !l in 
   (try  Stream.iter f s with
-  | _ -> f (sTR "error guarded_force_eval_stream"));
+  | _ -> f (Stream.next (str "error guarded_force_eval_stream")));
   Stream.of_list (List.rev !l);;
 
 
@@ -67,7 +67,7 @@ let rec string_of_path p =
               | i::p -> (string_of_int i)^" "^ (string_of_path p)
 ;;
 let print_path p =
-    output_results_nl [< 'sTR "Path:"; 'sTR  (string_of_path p)>]
+    output_results_nl (str "Path:" ++ str (string_of_path p))
 ;;
 
 let kill_proof_node index =
@@ -83,7 +83,8 @@ let kill_proof_node index =
 (*Message functions, the text of these messages is recognized by the protocols *)
 (*of CtCoq                                                                     *)
 let ctf_header message_name request_id =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR message_name; 'fNL; 'iNT request_id; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str message_name ++ fnl () ++ 
+  int request_id ++ fnl ();;
 
 let ctf_acknowledge_command request_id command_count opt_exn =
   let goal_count, goal_index = 
@@ -94,14 +95,14 @@ let ctf_acknowledge_command request_id command_count opt_exn =
         g_count, (min g_count !current_goal_index)
     else
       (0, 0) in
-  [< ctf_header "acknowledge" request_id;
-     'iNT command_count; 'fNL; 
-    'iNT goal_count; 'fNL; 
-    'iNT goal_index; 'fNL; 
-    'sTR !current_proof_name; 'fNL;
-    (match opt_exn with
-      Some e -> Errors.explain_exn e
-    | None -> [< >]); 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+  (ctf_header "acknowledge" request_id ++
+   int command_count ++ fnl () ++ 
+   int goal_count ++ fnl () ++ 
+   int goal_index ++ fnl () ++ 
+   str !current_proof_name ++ fnl () ++
+   (match opt_exn with
+	Some e -> Errors.explain_exn e
+      | None -> mt ()) ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 let ctf_undoResults = ctf_header "undo_results";;
 
@@ -116,35 +117,37 @@ let ctf_Location = ctf_header "location";;
 let ctf_StateMessage = ctf_header "state";;
 
 let ctf_PathGoalMessage () =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "single_goal"; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();;
 
 let ctf_GoalReqIdMessage = ctf_header "single_goal_state";;
 
 let ctf_NewStateMessage = ctf_header "fresh_state";;
 
-let ctf_SavedMessage () = [< 'fNL; 'sTR "message"; 'fNL; 'sTR "saved"; 'fNL >];;
+let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ str "saved" ++ fnl ();;
 
 let ctf_KilledMessage req_id ngoals =
- [< ctf_header "killed" req_id; 'iNT ngoals; 'fNL >];;
+ ctf_header "killed" req_id ++ int ngoals ++ fnl ();;
 
 let ctf_AbortedAllMessage () =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "aborted_all"; 'fNL >];;
+ fnl () ++ str "message" ++ fnl () ++ str "aborted_all" ++ fnl ();;
 
 let ctf_AbortedMessage request_id na =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "aborted_proof"; 'fNL; 'iNT request_id; 'fNL;
- 'sTR na; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str "aborted_proof" ++ fnl () ++ 
+  int request_id ++ fnl () ++
+  str na ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 
 let ctf_UserErrorMessage request_id stream =
- let stream = guarded_force_eval_stream stream in
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "user_error"; 'fNL; 'iNT request_id; 'fNL;
-  stream; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+  let stream = guarded_force_eval_stream stream in
+  fnl () ++ str "message" ++ fnl () ++ str "user_error" ++ fnl () ++ 
+  int request_id ++ fnl () ++
+  stream ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 
 let ctf_ResetInitialMessage () =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_initial"; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();;
 
-let ctf_ResetIdentMessage request_id str =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_ident"; 'fNL; 'iNT request_id; 'fNL;
- 'sTR str; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+let ctf_ResetIdentMessage request_id s =
+  fnl () ++ str "message" ++ fnl () ++ str "reset_ident" ++ fnl () ++ int request_id ++ fnl () ++
+  str s ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 
 type vtp_tree =
   | P_rl of ct_RULE_LIST
@@ -175,7 +178,7 @@ let break_happened = ref false;;
 let output_results stream vtp_tree =
     let _ = Sys.signal Sys.sigint
        (Sys.Signal_handle(fun i -> (break_happened := true;()))) in
-    mSG stream;
+    msg stream;
     match vtp_tree with
       Some t -> print_tree t
     | None -> ();;
@@ -184,7 +187,7 @@ let output_results_nl stream =
     let _ = Sys.signal Sys.sigint
        (Sys.Signal_handle(fun i -> break_happened := true;()))
     in
-    mSGNL stream;;
+    msgnl stream;;
 
 
 let rearm_break () =
@@ -216,7 +219,7 @@ let show_nth n =
   try
     let pf = proof_of_pftreestate (get_pftreestate()) in
     if (!text_proof_flag<>"off") then
-(*      errorlabstrm "debug" [< 'sTR "text printing unplugged" >]*)
+(*      errorlabstrm "debug" [< str "text printing unplugged" >]*)
        (if n=0
 	   then output_results (ctf_TextMessage !global_request_id)
                                (Some (P_text (show_proof !text_proof_flag [])))
@@ -255,14 +258,14 @@ let add_search (global_reference:global_reference) assumptions cstr =
                   CT_coerce_ID_to_FORMULA(
                     CT_ident ("Error printing" ^ id_string))) in
     ctv_SEARCH_LIST:= ast::!ctv_SEARCH_LIST
-  with e -> mSGNL [< 'sTR "add_search raised an exception" >]; raise e;;
+  with e -> msgnl (str "add_search raised an exception"); raise e;;
 
 let make_error_stream node_string =
- [< 'sTR "The syntax of "; 'sTR node_string;
- 'sTR " is inconsistent with the vernac interpreter entry" >];;
+  str "The syntax of " ++ str node_string ++
+  str " is inconsistent with the vernac interpreter entry";;
 
 let ctf_EmptyGoalMessage id =
- [< 'fNL; 'sTR "Empty Goal is a no-op.  Fun oh fun."; 'fNL >];;
+  fnl () ++ str "Empty Goal is a no-op.  Fun oh fun." ++ fnl ();;
 
 
 let print_check (ast, judg) =
@@ -271,15 +274,17 @@ let print_check (ast, judg) =
      (try translate_constr (Global.env()) value 
       with UserError(f,str) ->
            raise(UserError(f,
-			   [< Ast.print_ast 
-				(ast_of_constr true (Global.env()) value);
-			      'fNL; str >]))) in
+			   Ast.print_ast 
+			     (ast_of_constr true (Global.env()) value) ++
+			   fnl () ++ str))) 
+ in
  let type_ct_ast =
      (try translate_constr (Global.env()) typ
       with UserError(f,str) ->
-           raise(UserError(f, [< Ast.print_ast (ast_of_constr true (Global.env())
-					       value);
-				 'fNL; str >]))) in
+           raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env())
+					       value) ++
+				 fnl () ++ str))) 
+ in
  ((ctf_SearchResults !global_request_id),
  (Some  (P_pl
   (CT_premises_list
@@ -318,16 +323,16 @@ let globcv = function
 let pbp_tac_pcoq =
     pbp_tac (function x -> 
       output_results
-  	[< 'fNL; 'sTR "message"; 'fNL; 'sTR "pbp_results"; 'fNL;
-	  'iNT !global_request_id;  'fNL>]
-       (Some (P_t(xlate_tactic x))));;
+  	(fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++
+	 int !global_request_id ++  fnl ())
+	(Some (P_t(xlate_tactic x))));;
 
 
 let dad_tac_pcoq =
   dad_tac(function x -> 
     output_results
-    [< 'fNL; 'sTR "message"; 'fNL; 'sTR "pbp_results"; 'fNL;
-       'iNT !global_request_id;  'fNL >]
+    (fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++
+       int !global_request_id ++  fnl ())
     (Some (P_t(xlate_tactic x))));;
 
 let search_output_results () =
@@ -346,8 +351,8 @@ let debug_tac2_pcoq = function
 	try
 	  let result = report_error ast the_goal the_ast the_path [] g in
 	  (errorlabstrm "DEBUG TACTIC"
-	    [< 'sTR "no error here "; 'fNL; pr_goal (sig_it g);
-	      'fNL; 'sTR "the tactic is"; 'fNL ; Printer.gentacpr ast >];
+	    (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++
+	     fnl () ++ str "the tactic is" ++ fnl ()  ++ Printer.gentacpr ast);
 	   result)
 	with
 	  e ->
@@ -481,9 +486,9 @@ let command_changes = [
 	    begin
 	      if kind = "LETTOP" && not(refining ()) then
 		errorlabstrm "StartProof"
-		  [< 'sTR
-                       "Let declarations can only be used in proof editing mode"
-		  >];
+		  (str
+                     "Let declarations can only be used in proof editing mode"
+		  );
 		let str = (string_of_id s) in
 		start_proof_com (Some s) stre c;
 		History.start_proof str;
@@ -563,7 +568,7 @@ let command_changes = [
 	 (function
 	     () ->
 	       errorlabstrm "Begin Silent" 
-		 [< 'sTR "not available in Centaur mode" >])
+		 (str "not available in Centaur mode"))
      | _ -> errorlabstrm "BeginSilent" (make_error_stream "BeginSilent")));
   
   ("EndSilent", 
@@ -572,7 +577,7 @@ let command_changes = [
 	 (function
 	     () ->
 	       errorlabstrm "End Silent"
-		 [< 'sTR "not available in Centaur mode" >])
+		 (str "not available in Centaur mode"))
      | _ -> errorlabstrm "EndSilent" (make_error_stream "EndSilent")));
   
   ("ABORT", 
@@ -633,7 +638,7 @@ let command_changes = [
 	 (function () -> 
 	   let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in
 	   output_results 
-	     [<'fNL; 'sTR "message"; 'fNL; 'sTR "PRINT_VALUE"; 'fNL >]
+	     (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ())
 	     (Some (P_cl results)))
      | _ -> errorlabstrm "PrintId" (make_error_stream "PrintId")));
   
@@ -646,7 +651,7 @@ let command_changes = [
 	   match kind with
 	   | "CHECK" -> print_check
 	   | "PRINTTYPE" ->
-	       errorlabstrm "PrintType" [< 'sTR "Not yet supported in CtCoq" >]
+	       errorlabstrm "PrintType" (str "Not yet supported in CtCoq")
 	   | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK") in
 	 (function () -> 
 	   let a,b = f (c, judgment_of_rawconstr evmap env c) in
@@ -692,8 +697,8 @@ let command_changes = [
 	 (fun () -> 
 	   let results = dad_rule_names() in
 	   output_results
-	     [< 'fNL; 'sTR "message"; 'fNL; 'sTR "dad_rule_names"; 'fNL;
-	       'iNT !global_request_id; 'fNL >]
+	     (fnl () ++ str "message" ++ fnl () ++ str "dad_rule_names" ++ fnl () ++
+	      int !global_request_id ++ fnl ())
 	     (Some (P_ids
 		      (CT_id_list
 			 (List.map (fun s -> CT_ident s) results)))))
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 7f2ea95a4..ce3817404 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -254,7 +254,7 @@ vinterp_add "AddDadRule"
               let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
               (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com)))
             | _ -> errorlabstrm "AddDadRule1"
-                    [< 'sTR "AddDadRule2">]);
+                    [< str "AddDadRule2">]);
 add_dad_rule "distributivity-inv"
 (Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])]))
 [2; 2]
diff --git a/contrib/interface/debug_tac.ml b/contrib/interface/debug_tac.ml
index b7542fa74..80d9d7201 100644
--- a/contrib/interface/debug_tac.ml
+++ b/contrib/interface/debug_tac.ml
@@ -183,7 +183,7 @@ and checked_thens: report_holder -> Coqast.t -> Coqast.t list -> tactic =
 	  | Recursive_fail tr -> Tree_fail tr
 	  | Fail -> Failed 1
 	  | _ -> errorlabstrm "check_thens"
-                  [< 'sTR "this case should not happen in check_thens">])::
+                  (str "this case should not happen in check_thens"))::
 	  !report_holder);
       result)
 
@@ -297,8 +297,8 @@ let rec reconstruct_success_tac ast =
 	| _ ->
 	    errorlabstrm
 	      "this error case should not happen on an unknown tactic"
-              [< 'sTR "error in reconstruction with "; 'fNL;
-		(gentacpr ast) >]);;
+              (str "error in reconstruction with " ++ fnl () ++
+	       (gentacpr ast)));;
 	  
 
 let rec path_to_first_error = function
@@ -332,15 +332,16 @@ let debug_tac = function
       	let clean_ast = expand_tactic ast in
       	let report_tree =
           try List.hd !report with
-	    Failure "hd" -> (mSGNL [< 'sTR "report is empty" >]; Failed 1) in
+	    Failure "hd" -> (msgnl (str "report is empty"); Failed 1) in
       	let success_tac = 
 	  reconstruct_success_tac clean_ast report_tree in
         let compact_success_tac =
 	  flatten_then success_tac in
-      	mSGNL [< 'fNL; 'sTR "=========    Successful tactic    ============="; 
-                 'fNL;
-	      	gentacpr compact_success_tac; 'fNL;
-	      	'sTR "========= End of successful tactic ============">];
+      	msgnl (fnl () ++
+	       str "=========    Successful tactic    =============" ++
+               fnl () ++
+	       gentacpr compact_success_tac ++ fnl () ++
+	       str "========= End of successful tactic ============");
       	result)
   | _ -> error "wrong arguments for debug_tac";;
 
@@ -427,10 +428,9 @@ let rec report_error
 	    with
 	      e ->
 		if !the_count > 1 then
-		  mSGNL
-		    [< 'sTR "in branch no "; 'iNT !the_count; 
-		      'sTR " after tactic ";
-		      gentacpr a >];
+		  msgnl
+		    (str "in branch no " ++ int !the_count ++
+		     str " after tactic " ++ gentacpr a);
 		raise e)
     | Node(_, "TACTICLIST", a::b::c::tl) ->
 	report_error (ope("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
@@ -458,16 +458,16 @@ let descr_first_error = function
 	let the_path = ref ([] : int list) in
 	try
 	  let result = report_error ast the_goal the_ast the_path [] g in
-	  mSGNL [< 'sTR "no Error here" >];
+	  msgnl (str "no Error here");
 	  result
 	with
 	  e ->
-	    (mSGNL [< 'sTR "Execution of this tactic raised message " ; 'fNL;
-		     'fNL; Errors.explain_exn e; 'fNL;
-		     'fNL; 'sTR "on goal" ; 'fNL;
-		     pr_goal (sig_it (strip_some !the_goal)); 'fNL;
-		     'sTR "faulty tactic is"; 'fNL; 'fNL;
-		     gentacpr (flatten_then !the_ast); 'fNL >];
+	    (msgnl (str "Execution of this tactic raised message " ++ fnl () ++
+		    fnl () ++ Errors.explain_exn e ++ fnl () ++
+		    fnl () ++ str "on goal"  ++ fnl () ++
+		    pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
+		    str "faulty tactic is" ++ fnl () ++ fnl () ++
+		    gentacpr (flatten_then !the_ast) ++ fnl ());
 	     tclIDTAC g))
   | _ -> error "wrong arguments for descr_first_error";;
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index e96106368..a7d5644f0 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -56,8 +56,8 @@ let impl_args_to_string = function
 let implicit_args_id_to_ast_list id l ast_list = 
     (match impl_args_to_string l with
            None -> ast_list
-         | Some(s) -> (str("For " ^ (string_of_id id)))::
-                       (str s)::
+         | Some(s) -> (string ("For " ^ (string_of_id id)))::
+                      (string s)::
                        ast_list);;
 
 (* This function construct an ast to enumerate the implicit positions for an
@@ -125,7 +125,7 @@ let mutual_to_ast_list sp mib =
     Array.fold_right
       (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
   (ope("MUTUALINDUCTIVE",
-	  [str (if mib.mind_finite then "Inductive" else "CoInductive");
+	  [string (if mib.mind_finite then "Inductive" else "CoInductive");
 	  ope("VERNACARGLIST", ast_list)])::
      (implicit_args_to_ast_list sp mipv));;
 
@@ -135,11 +135,11 @@ let constr_to_ast v =
 let implicits_to_ast_list implicits =
     (match (impl_args_to_string implicits) with
                   None -> []
-                | Some s -> [ope("COMMENT", [str s])]);;
+                | Some s -> [ope("COMMENT", [string s])]);;
 
 let make_variable_ast name typ implicits =
    (ope("VARIABLE",
-    [str "VARIABLE";
+    [string "VARIABLE";
      ope("BINDERLIST",
          [ope("BINDER",
             [(constr_to_ast (body_of_type typ));
@@ -148,7 +148,7 @@ let make_variable_ast name typ implicits =
     
 let make_definition_ast name c typ implicits =
  (ope("DEFINITION",
-      [str "DEFINITION";
+      [string "DEFINITION";
        nvar name;
        ope("COMMAND",
            [ope("CAST",
@@ -193,8 +193,8 @@ let leaf_entry_to_ast_list (sp,lobj) =
   | (_, "INDUCTIVE") -> inductive_to_ast_list sp
   | (_, s) -> 
       errorlabstrm 
-      	"print" [< 'sTR ("printing of unrecognized object " ^
-			 s ^ " has been required") >];;
+      	"print" (str ("printing of unrecognized object " ^
+		      s ^ " has been required"));;
 
 
 
@@ -232,10 +232,11 @@ let name_to_ast (qid:Nametab.qualid) =
 	    try
 	      let sp = Syntax_def.locate_syntactic_definition qid in
 		errorlabstrm "print"
-      		  [< 'sTR "printing of syntax definitions not implemented" >]
+      		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
 	      errorlabstrm "print"
-		[< Nametab.pr_qualid qid;
-		   'sPC; 'sTR "not a defined object" >] in
-    ope("vernac_list", l);;
+		(Nametab.pr_qualid qid ++
+		 spc () ++ str "not a defined object")
+  in
+  ope("vernac_list", l);;
 
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 6b2e38873..fad5c1e34 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -2,10 +2,10 @@ open Util;;
 
 open System;;
 
-open Pp;;
-
 open Ctast;;
 
+open Pp;;
+
 open Library;;
 
 open Ascent;;
@@ -43,15 +43,15 @@ let print_parse_results n msg =
   flush stdout;;
 
 let ctf_SyntaxErrorMessage reqid pps =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "syntax_error"; 'fNL; 'iNT reqid; 'fNL;
-   pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+ (fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ int reqid ++ fnl () ++
+   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 let ctf_SyntaxWarningMessage reqid pps =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "syntax_warning"; 'fNL; 'iNT reqid; 'fNL;
-   pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+ (fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ int reqid ++ fnl () ++
+   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 let ctf_FileErrorMessage reqid pps =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "file_error"; 'fNL; 'iNT reqid; 'fNL;
-   pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+ (fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ int reqid ++ fnl () ++
+   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 (*In the code for CoqV6.2, the require_module call is encapsulated in
   a function "without_mes_ambig".  Here I have supposed that this
@@ -60,7 +60,7 @@ let try_require_module import specif name fname =
  try Library.require_module (if specif = "UNSPECIFIED" then None
   else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
  with
- | e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];;
+ | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
 
 let execute_when_necessary ast =
  (match ast with
@@ -79,11 +79,12 @@ let execute_when_necessary ast =
   | _ -> ()); ast;;
 
 let parse_to_dot =
-  let rec dot = parser
-      [< '("", ".") >] -> ()
-    | [< '("EOI", "") >] -> raise End_of_file
-    | [< '_; s >] -> dot s
-  in Gram.Entry.of_parser "Coqtoplevel.dot" dot;;
+  let rec dot st = match Stream.next st with
+    | ("", ".") -> ()
+    | ("EOI", "") -> raise End_of_file
+    | _ -> dot st
+  in 
+  Gram.Entry.of_parser "Coqtoplevel.dot" dot;;
 
 let rec discard_to_dot stream =
   try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with
@@ -149,11 +150,11 @@ let parse_command_list reqid stream string_list =
         with
         | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> 
           begin
-             mSGNL (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e));
+             msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e));
              try
                 discard_to_dot stream;
-                mSGNL [< 'sTR "debug"; 'fNL; 'iNT this_pos; 'fNL; 'iNT 
-                  (Stream.count stream) >];
+                msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ int 
+                  (Stream.count stream));
                 Some( Node(l, "PARSING_ERROR",
                         List.map Ctast.str
                         (get_substring_list string_list this_pos
@@ -175,7 +176,7 @@ let parse_command_list reqid stream string_list =
     | None -> [] in
     match parse_whole_stream () with
     | first_one::tail -> (P_cl (CT_command_list(first_one, tail)))
-    | [] -> raise (UserError ("parse_string", [< 'sTR "empty text." >]));;
+    | [] -> raise (UserError ("parse_string", (str "empty text.")));;
 
 (*When parsing a string using a phylum, the string is first transformed
   into a Coq Ast using the regular Coq parser, then it is transformed into
@@ -215,12 +216,12 @@ let parse_string_action reqid phylum char_stream string_list =
  with
  | Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
     flush_until_end_of_stream char_stream;
-    mSGNL (ctf_SyntaxErrorMessage reqid
+    msgnl (ctf_SyntaxErrorMessage reqid
               (Errors.explain_exn 
                  (Stdpp.Exc_located(l,Stream.Error "match failure"))))
  | e ->
     flush_until_end_of_stream char_stream;
-    mSGNL (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));;
+    msgnl (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));;
 
 
 let quiet_parse_string_action char_stream =
@@ -247,10 +248,10 @@ let parse_file_action reqid file_name =
                 this_ast
               with
             | Stdpp.Exc_located(l,Stream.Error txt ) -> 
-                 mSGNL (ctf_SyntaxWarningMessage reqid
-                [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL;
+                 msgnl (ctf_SyntaxWarningMessage reqid
+                (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
                    Errors.explain_exn 
-                      (Stdpp.Exc_located(l,Stream.Error txt)) >]);
+                      (Stdpp.Exc_located(l,Stream.Error txt))));
                  let rec discard_to_dot () =
                  try Gram.Entry.parse parse_to_dot (Gram.parsable stream)
                  with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot()
@@ -276,18 +277,18 @@ let parse_file_action reqid file_name =
       | first_one :: tail ->
        print_parse_results reqid
           (P_cl (CT_command_list (first_one, tail)))
-      | [] -> raise (UserError ("parse_file_action", [< 'sTR "empty file." >]))
+      | [] -> raise (UserError ("parse_file_action", (str "empty file.")))
  with
  | Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
- mSGNL
+ msgnl
   (ctf_SyntaxErrorMessage reqid
-  [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL;
-  Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")) >])
+  (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
+  Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure"))))
  | e ->
- mSGNL
+ msgnl
   (ctf_SyntaxErrorMessage reqid
-  [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL;
-  Errors.explain_exn e >]);;
+  (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
+  Errors.explain_exn e));;
 
 (* This function is taken from Mltop.add_path *)
 
@@ -297,7 +298,7 @@ let add_path dir coq_dirpath =
       Library.add_load_path_entry (dir,coq_dirpath)
     end
   else
-    wARNING [< 'sTR ("Cannot open " ^ dir) >]
+    msg_warning (str ("Cannot open " ^ dir))
 
 let convert_string d =
   try Names.id_of_string d
@@ -315,7 +316,7 @@ let add_rec_path dir coq_dirpath =
       List.iter Library.add_load_path_entry dirs
     end
     else
-      wARNING [< 'sTR ("Cannot open " ^ dir) >];;
+      msg_warning (str ("Cannot open " ^ dir));;
 
 let add_path_action reqid string_arg =
   let directory_name = glob string_arg in
@@ -325,30 +326,30 @@ let add_path_action reqid string_arg =
     end;;
 
 let print_version_action () =
-  mSGNL [< >];
-  mSGNL [< 'sTR "$Id$" >];;
+  msgnl (mt ());
+  msgnl (str "$Id$");;
 
 let load_syntax_action reqid module_name =
- mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >];
+ msg (str "loading " ++ str module_name ++ str "... ");
  try
       (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
       read_module qid;
-      mSG [< 'sTR "opening... ">];
+      msg (str "opening... ");
       let fullname = Nametab.locate_loaded_library qid in 
       import_module fullname; 
-      mSGNL [< 'sTR "done"; 'fNL >];
+      msgnl (str "done" ++ fnl ());
       ())
  with
  | UserError (label, pp_stream) ->
  (*This one may be necessary to make sure that the message won't be indented *)
- mSGNL [< >];
- mSGNL
-  [< 'fNL; 'sTR "error while loading syntax module "; 'sTR module_name;
-  'sTR ": "; 'sTR label; 'fNL; pp_stream >]
+ msgnl (mt ());
+ msgnl
+  (fnl () ++ str "error while loading syntax module " ++ str module_name ++
+  str ": " ++ str label ++ fnl () ++ pp_stream)
  | e ->
-  mSGNL [< >];
-  mSGNL
-   [< 'fNL; 'sTR "message"; 'fNL; 'sTR "load_error"; 'fNL; 'iNT reqid; 'fNL >];
+  msgnl (mt ());
+  msgnl
+   (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ int reqid ++ fnl ());
   ();;
 
 let coqparser_loop inchan =
@@ -370,12 +371,12 @@ Libobject.relax true;
        if Sys.file_exists coqdir then
 	 coqdir
        else
-	 (mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in
+	 (msgnl (str "could not find the value of COQDIR"); exit 1) in
      begin
        add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]);
        add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]);
        add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]);
-       List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
+       List.iter (fun a -> msgnl (str a)) (get_load_path())
      end;
 (try 
   (match create_entry (get_univ "nat") "number" ETast with
@@ -387,10 +388,10 @@ Libobject.relax true;
 	    (fun s loc ->
 		 Node((0,0),"XTRA",[Str((0,0),"omega_integer_for_ctcoq");
 				 Num((0,0),int_of_string s)]))]]
-   | _ -> mSGNL [< 'sTR "unpredicted behavior of Grammar.extend" >])
+   | _ -> msgnl (str "unpredicted behavior of Grammar.extend"))
 
  with
-   e -> mSGNL [< 'sTR "could not add a parser for numbers" >]);
+   e -> msgnl (str "could not add a parser for numbers"));
 (let vernacrc =
    try
      Sys.getenv "VERNACRC"
@@ -406,28 +407,28 @@ Libobject.relax true;
    with
      | End_of_file -> ()
      | e ->
-	 (mSGNL (Errors.explain_exn e);
-	  mSGNL [< 'sTR "could not load the VERNACRC file" >]);
+	 (msgnl (Errors.explain_exn e);
+	  msgnl (str "could not load the VERNACRC file"));
 	 try
-	   mSGNL [< 'sTR vernacrc >]
+	   msgnl (str vernacrc)
 	 with
 	     e -> ());
 (try let user_vernacrc =
    try Some(Sys.getenv "USERVERNACRC")
    with
      | Not_found as e ->
-	 mSGNL [< 'sTR "no .vernacrc file" >]; None in
+	 msgnl (str "no .vernacrc file"); None in
    (match user_vernacrc with
       	Some f -> coqparser_loop (open_in f)
       | None -> ())
  with
    | End_of_file -> ()
    | e ->
-       mSGNL (Errors.explain_exn e);
-       mSGNL [< 'sTR "error in your .vernacrc file" >]);
-mSGNL [< 'sTR "Starting Centaur Specialized Parser Loop" >];
+       msgnl (Errors.explain_exn e);
+       msgnl (str "error in your .vernacrc file"));
+msgnl (str "Starting Centaur Specialized Parser Loop");
 try
   coqparser_loop stdin
 with 
   | End_of_file -> ()
-  | e -> mSGNL(Errors.explain_exn e))
+  | e -> msgnl(Errors.explain_exn e))
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5bfad2f52..c23394e8c 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1806,7 +1806,7 @@ let show_proof lang gpath =
     ;;
 
 let show_nproof path =
-  pP (sp_print (sph [spi; show_proof "fr" path]));;
+  pp (sp_print (sph [spi; show_proof "fr" path]));;
 
 vinterp_add "ShowNaturalProof"
 	    (fun _ ->
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index e3bca2243..b689620e3 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -120,31 +120,31 @@ let sphv l =
 
 let rec prlist_with_sep f g l =
     match l with 
-      [] -> hOV 0 [< >]
-     |x::l1 -> hOV 0 [< (g x); (f ()); (prlist_with_sep f g l1)>]
+      [] -> hov 0 (mt ())
+     |x::l1 -> hov 0 ((g x) ++ (f ()) ++ (prlist_with_sep f g l1))
 ;;
    
 let rec sp_print x = 
    match x with
-     CT_coerce_ID_to_TEXT (CT_ident s)
-     -> (match s with
-       "\n" -> [< 'fNL >]
-     | "Retour chariot pour Show proof" -> [< 'fNL >]
-     |_ -> [< 'sTR s >])
-   | CT_text_formula  f -> [< prterm (Hashtbl.find ct_FORMULA_constr f) >]
-  |  CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
-	      CT_text_path (CT_signed_int_list p);
-              CT_coerce_ID_to_TEXT (CT_ident "goal");
-	      g] ->
+     | CT_coerce_ID_to_TEXT (CT_ident s)
+       -> (match s with
+	     | "\n" -> fnl ()
+	     | "Retour chariot pour Show proof" -> fnl ()
+	     |_ -> str s)
+     | CT_text_formula  f -> prterm (Hashtbl.find ct_FORMULA_constr f)
+     | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
+		   CT_text_path (CT_signed_int_list p);
+		   CT_coerce_ID_to_TEXT (CT_ident "goal");
+		   g] ->
       let p=(List.map (fun y -> match y with
 	                 (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
-      h 0 [<  'sTR "<b>"; sp_print g; 'sTR "</b>">]
+      h 0 (str "<b>" ++ sp_print g ++ str "</b>")
  |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "uselemma");
               CT_coerce_ID_to_TEXT (CT_ident intro);
 	      l;g] ->
-      h 0 [< 'sTR ("<i>("^intro^" "); sp_print l; 'sTR ")</i>"; sp_print g>]
+      h 0 (str ("<i>("^intro^" ") ++ sp_print l ++ str ")</i>" ++ sp_print g)
  |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp");
 	      CT_text_path (CT_signed_int_list p);
 	      CT_coerce_ID_to_TEXT (CT_ident hyp);
@@ -153,7 +153,7 @@ let rec sp_print x =
 	                  (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
-            h 0 [< 'sTR hyp>]
+            h 0 (str hyp)
 
   |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp_with_type");
 	      CT_text_path (CT_signed_int_list p);
@@ -163,23 +163,23 @@ let rec sp_print x =
                          (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
-      h 0 [< sp_print g; 'sPC; 'sTR "<i>("; 'sTR hyp;'sTR ")</i>">]   
+      h 0 (sp_print g ++ spc () ++ str "<i>(" ++ str hyp ++ str ")</i>")   
 
   | CT_text_h l ->
-      h 0 [< prlist_with_sep (fun () -> [< >])
-		(fun y -> sp_print y) l>]
+      h 0 (prlist_with_sep (fun () -> mt ())
+	     (fun y -> sp_print y) l)
   | CT_text_v l ->
-      v 0 [< prlist_with_sep (fun () -> [< >])
-		(fun y -> sp_print y) l>]
+      v 0 (prlist_with_sep (fun () -> mt ())
+		(fun y -> sp_print y) l)
   | CT_text_hv l ->
-      h 0 [< prlist_with_sep (fun () -> [<>])
-		(fun y -> sp_print y) l>]
+      h 0 (prlist_with_sep (fun () -> mt ())
+	     (fun y -> sp_print y) l)
   | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "shrink");
 	      CT_text_op [CT_coerce_ID_to_TEXT (CT_ident info); t]]  ->
-                   h 0 [< 'sTR ("("^info^": "); sp_print t ;'sTR ")" >]
+                   h 0 (str ("("^info^": ") ++ sp_print t ++ str ")")
   | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "root_of_text_proof");
               t]->
                     sp_print t 
-  | _ -> [< 'sTR "..." >]
+  | _ -> str "..."
 ;;
   
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index 75cd7db38..c691ff912 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -56,12 +56,12 @@ let dbize_sp =
       | Invalid_argument _ | Failure _ ->
       anomaly_loc
        (loc, "Translate.dbize_sp (taken from Astterm)",
-       [< 'sTR "malformed section-path" >])
+       [< str "malformed section-path" >])
     end
     | ast ->
      anomaly_loc
       (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)",
-      [< 'sTR "not a section-path" >]);;
+      [< str "not a section-path" >]);;
 *)
 
 (* dead code:
@@ -120,8 +120,9 @@ let translate_sign env =
     fold_named_context
       (fun env (id,v,c) l -> 
 	 (CT_premise(CT_ident(string_of_id id), translate_constr env c))::l)
-      env [] in
-    CT_premises_list l;;
+      env ~init:[] 
+  in
+  CT_premises_list l;;
        
 (* the function rev_and_compact performs two operations:
    1- it reverses the list of integers given as argument