compat ocaml 3.03

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

10 files changed, 54 insertions, 48 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3152478abb..7f6f05d11b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -176,7 +176,7 @@ let pred_case_ml_onebranch loc env sigma isrec indt (i,fj) =
 open Pp
 
 let mssg_may_need_inversion () =
-  [< 'sTR "This pattern-matching is not exhaustive.">]
+  str "This pattern-matching is not exhaustive."
 
 let mssg_this_case_cannot_occur () =
   "This pattern-matching is not exhaustive."
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 77dff358b0..952bb98220 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -257,7 +257,7 @@ let coercion_value i =
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
 
-let path_printer = ref (fun _ -> [< 'sTR "<a class path>" >] 
+let path_printer = ref (fun _ -> str "<a class path>"
                         : (int * int) * inheritance_path -> std_ppcmds)
 
 let install_path_printer f = path_printer := f
@@ -265,8 +265,8 @@ let install_path_printer f = path_printer := f
 let print_path x = !path_printer x
 
 let message_ambig l = 
-  [< 'sTR"Ambiguous paths:"; 'sPC;
-     prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >]
+  (str"Ambiguous paths:" ++ spc () ++
+   prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l)
 
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit 
                          coercion,source,target *)
@@ -315,7 +315,7 @@ let add_coercion_in_graph (ic,source,target) =
       old_inheritance_graph 
   end;
   if (!ambig_paths <> []) && is_verbose () && is_mes_ambig() then 
-    pPNL (message_ambig !ambig_paths)
+    ppnl (message_ambig !ambig_paths)
 
 type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ
 
@@ -337,7 +337,7 @@ let (inCoercion,outCoercion) =
                     cache_function = cache_coercion;
                     export_function = (function x -> Some x) })
 
-let declare_coercion coef v stre isid cls clt ps =
+let declare_coercion coef v stre ~isid ~src:cls ~target:clt ~params:ps =
   Lib.add_anonymous_leaf
     (inCoercion
        ((coef,
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index ecdce7543a..3861d8d356 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -71,7 +71,7 @@ val strength_of_cl : cl_typ -> strength
 
 (*s [declare_coercion] adds a coercion in the graph of coercion paths *)
 val declare_coercion : 
-  coe_typ -> value:unsafe_judgment -> strength:strength -> isid:bool ->
+  coe_typ -> unsafe_judgment -> strength -> isid:bool ->
       src:cl_typ -> target:cl_typ -> params:int -> unit
 
 (*s Access to coercions infos *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b634b04435..111e5a514e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -32,8 +32,8 @@ let encode_inductive ref =
     | IndRef indsp -> indsp
     | _ ->
         errorlabstrm "indsp_of_id"
-          [< pr_global_env (Global.env()) ref;
-	     'sTR" is not an inductive type" >] in
+          (pr_global_env (Global.env()) ref ++
+	     str" is not an inductive type") in
   let (mib,mip) = Global.lookup_inductive indsp in
   let constr_lengths = Array.map List.length mip.mind_listrec in
   (indsp,constr_lengths)
@@ -67,7 +67,7 @@ module PrintingCasesMake =
     let encode = encode_inductive
     let check (_,lc) =
       if not (Test.test lc) then 
-	errorlabstrm "check_encode" [< 'sTR Test.error_message >]
+	errorlabstrm "check_encode" (str Test.error_message)
     let printer (ind,_) =
       pr_id (basename (path_of_inductive (Global.env()) ind))
     let key = Goptions.SecondaryTable ("Printing",Test.field)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a56e87b2e5..a53ecf5355 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -308,8 +308,9 @@ let make_evar_instance_with_rel env =
       (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*))
       env ~init:[] in
   snd (fold_rel_context
-    (fun env (_,b,_) (i,l) -> (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
-    env (n,vars))
+	 (fun env (_,b,_) (i,l) -> 
+	    (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
+	 env ~init:(n,vars))
 
 let make_subst env args =
   snd (fold_named_context
@@ -318,7 +319,7 @@ let make_subst env args =
 	 | (* None *) _ , a::rest -> (rest, (id,a)::l)
 (*	 | Some _, _ -> g*)
 	 | _ -> anomaly "Instance does not match its signature")
-    env (List.rev args,[]))
+    env ~init:(List.rev args,[]))
 
 (* [new_isevar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
@@ -335,7 +336,7 @@ let push_rel_context_to_named_context env =
 	add_named_decl (id,option_app (substl subst) c,
                         type_app (substl subst) t)
 	  sign))
-    (rel_context env) ([],ids_of_named_context sign0,sign0)
+    (rel_context env) ~init:([],ids_of_named_context sign0,sign0)
   in (subst, reset_with_named_context sign env)
 
 let new_isevar isevars env typ =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 3c5e17b09a..392b4fc847 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -533,7 +533,7 @@ let declare_one_elimination ind =
           const_entry_type = None;
           const_entry_opaque = false }, 
        NeverDischarge) in
-    Options.if_verbose pPNL [< 'sTR na; 'sTR " is defined" >]
+    Options.if_verbose ppnl (str na ++ str " is defined")
   in
   let env = Global.env () in
   let sigma = Evd.empty in
@@ -575,9 +575,9 @@ let lookup_eliminator ind_sp s =
     try construct_reference env id
     with Not_found ->
       errorlabstrm "default_elim"
-	[< 'sTR "Cannot find the elimination combinator :";
-           pr_id id; 'sPC;
-	   'sTR "The elimination of the inductive definition :";
-           pr_id base; 'sPC; 'sTR "on sort "; 
-           'sPC; print_sort (new_sort_in_family s) ;
-	   'sTR " is probably not allowed" >]
+	(str "Cannot find the elimination combinator :" ++
+           pr_id id ++ spc () ++
+	   str "The elimination of the inductive definition :" ++
+           pr_id base ++ spc () ++ str "on sort " ++ 
+           spc () ++ print_sort (new_sort_in_family s) ++
+	   str " is probably not allowed")
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dee738a777..2971ba430f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -207,7 +207,7 @@ let rec pretype tycon env isevars lvar lmeta = function
             Not_found ->
 	      user_err_loc
 		(loc,"pretype",
-		 [< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >])
+		 str "Metavariable " ++ int n ++ str " is unbound")
       in inh_conv_coerce_to_tycon loc env isevars j tycon
 	   
   | RHole loc ->
@@ -220,7 +220,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 		| Some loc -> 
 		    user_err_loc
 		      (loc,"pretype",
-		       [< 'sTR "Cannot infer a term for this placeholder" >])))
+		       (str "Cannot infer a term for this placeholder"))))
 
   | RRec (loc,fixkind,names,lar,vdef) ->
       let larj =
@@ -420,7 +420,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       j
       (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
     else
-      user_err_loc (loc,"pretype",[< 'sTR "Not a constr tagged Dynamic" >])
+      user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
 
 (* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *)
 and pretype_type valcon env isevars lvar lmeta = function
@@ -471,7 +471,7 @@ let check_evars fail_evar initial_sigma sigma c =
 	  if not (Evd.in_dom initial_sigma ev) then
 	    (if fail_evar then
 	      errorlabstrm "whd_ise"
-		[< 'sTR"There is an unknown subterm I cannot solve" >]
+		(str"There is an unknown subterm I cannot solve")
 	    else (* try to avoid duplication *)
               (if not (List.exists (fun (k',_) -> k=k') !metamap) then
 	        metamap := (k, existential_type sigma k) :: !metamap))
@@ -534,7 +534,7 @@ let understand_type sigma env c =
   let _,c = ise_infer_type_gen true sigma env [] [] c in
   c.utj_val
 
-let understand_gen sigma env lvar lmeta exptyp c =
+let understand_gen sigma env lvar lmeta ~expected_type:exptyp c =
   let _, c = ise_infer_gen true sigma env lvar lmeta exptyp c in
   c.uj_val
 
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 381a40ee66..f13f31de0a 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -33,7 +33,7 @@ let add_syntax_constant sp c =
 let cache_syntax_constant (sp,c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
-      [< pr_id (basename sp); 'sTR " already exists" >];
+      (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant sp c;
   Nametab.push_syntactic_definition sp;
   Nametab.push_short_name_syntactic_definition sp
@@ -41,7 +41,7 @@ let cache_syntax_constant (sp,c) =
 let load_syntax_constant (sp,c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
-      [< pr_id (basename sp); 'sTR " already exists" >];
+      (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant sp c;
   Nametab.push_syntactic_definition sp
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 6c38f6d9a8..2f2f7e7531 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -30,9 +30,9 @@ let set_transparent_const sp =
   let cb = Global.lookup_constant sp in
   if cb.const_body <> None & cb.const_opaque then
     errorlabstrm "set_transparent_const"
-      [< 'sTR "Cannot make"; 'sPC; 
-         Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp);
-         'sPC; 'sTR "transparent because it was declared opaque." >];
+      (str "Cannot make" ++ spc () ++ 
+         Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp) ++
+         spc () ++ str "transparent because it was declared opaque.");
   Conv_oracle.set_transparent_const sp
 
 let set_opaque_var      = Conv_oracle.set_opaque_var
@@ -601,7 +601,7 @@ let rec substlin env name n ol c =
           with
 	      NotEvaluableConst _ ->
 		errorlabstrm "substlin"
-		  [< pr_sp const; 'sTR " is not a defined constant" >]
+		  (pr_sp const ++ str " is not a defined constant")
         else 
 	  ((n+1), ol, c)
 
@@ -611,7 +611,7 @@ let rec substlin env name n ol c =
 	    | (_,Some c,_) -> (n+1, List.tl ol, c)
 	    | _ -> 
 		errorlabstrm "substlin"
-		  [< pr_id id; 'sTR " is not a defined constant" >]
+		  (pr_id id ++ str " is not a defined constant")
         else 
 	  ((n+1), ol, c)
 
@@ -829,14 +829,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	    elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l)
 	  else
 	     errorlabstrm "tactics__reduce_to_mind"
-	       [< 'sTR"Not an inductive definition" >]
+	       (str"Not an inductive definition")
       | _ ->
           (try 
 	     let t' = nf_betaiota (one_step_reduce env sigma t) in 
 	     elimrec env t' l
            with NotStepReducible ->
 	     errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product" >])
+               (str"Not an inductive product"))
   in
   elimrec env t []
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 04cbd0d19e..97e8f68cc5 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -18,10 +18,10 @@ open Nametab
 open Sign
 
 let print_sort = function
-  | Prop Pos -> [< 'sTR "Set" >]
-  | Prop Null -> [< 'sTR "Prop" >]
-(*  | Type _ -> [< 'sTR "Type" >] *)
-  | Type u -> [< 'sTR "Type("; Univ.pr_uni u; 'sTR ")" >]
+  | Prop Pos -> (str "Set")
+  | Prop Null -> (str "Prop")
+(*  | Type _ -> (str "Type") *)
+  | Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")")
 
 let current_module = ref empty_dirpath
 
@@ -41,10 +41,10 @@ let new_sort_in_family = function
 
 
 (* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
-let prod_it = List.fold_left (fun c (n,t)  -> mkProd (n, t, c))
+let prod_it ~init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
 
 (* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *)
-let lam_it = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c))
+let lam_it ~init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
 
 (* [Rel (n+m);...;Rel(n+1)] *)
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
@@ -104,12 +104,17 @@ let mkProd_wo_LetIn (na,body,t) c =
     | None -> mkProd (na, body_of_type t, c)
     | Some b -> subst1 b c
 
-let it_mkProd_wo_LetIn   = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
-let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+let it_mkProd_wo_LetIn ~init = 
+  List.fold_left (fun c d -> mkProd_wo_LetIn d c) init
 
-let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+let it_mkProd_or_LetIn ~init = 
+  List.fold_left (fun c d -> mkProd_or_LetIn d c) init
 
-let it_named_context_quantifier f = List.fold_left (fun c d -> f d c)
+let it_mkLambda_or_LetIn ~init =
+  List.fold_left (fun c d -> mkLambda_or_LetIn d c) init
+
+let it_named_context_quantifier f ~init = 
+  List.fold_left (fun c d -> f d c) init
 
 let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
 let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
@@ -469,7 +474,7 @@ let subst_term_occ locs c t =
   else 
     let (nbocc,t') = subst_term_occ_gen locs 1 c t in
     if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
-      errorlabstrm "subst_term_occ" [< 'sTR "Too few occurences" >];
+      errorlabstrm "subst_term_occ" (str "Too few occurences");
     t'
 
 let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
@@ -484,7 +489,7 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
 	  let (nbocc,body') = subst_term_occ_gen locs 1 c body in
 	  let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in
 	  if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
-	    errorlabstrm "subst_term_occ_decl" [< 'sTR "Too few occurences" >];
+	    errorlabstrm "subst_term_occ_decl" (str "Too few occurences");
 	  (id,Some body',t')
 
 
@@ -709,7 +714,7 @@ let lift_rel_context n sign =
   in
   liftrec (rel_context_length sign) sign
 
-let fold_named_context_both_sides = list_fold_right_and_left
+let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
 
 let rec mem_named_context id = function
   | (id',_,_) :: _ when id=id' -> true