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, 51 insertions, 48 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 56ef7cafb2..7cac9e5969 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -32,9 +32,9 @@ let reset () =
   beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0
 
 let stop() =
-  mSGNL [< 'sTR"[Reds: beta=";'iNT !beta; 'sTR" delta="; 'iNT !delta;
-	   'sTR" zeta="; 'iNT !zeta; 'sTR" evar="; 'iNT !evar;
-           'sTR" iota="; 'iNT !iota; 'sTR" prune="; 'iNT !prune; 'sTR"]" >]
+  msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+	 str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++
+         str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]")
 
 let incr_cnt red cnt =
   if red then begin
@@ -383,7 +383,7 @@ let defined_rels flags env =
 	 match b with
 	   | None -> (i+1, subs)
 	   | Some body -> (i+1, (i,body) :: subs))
-      env (0,[])
+      env ~init:(0,[])
 (*  else (0,[])*)
 
 let create mk_cl flgs env =
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3b901a1acf..0313d4d467 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -36,13 +36,13 @@ type recipe = {
 
 let failure () =
   anomalylabstrm "generic__modify_opers"
-    [< 'sTR"An oper which was never supposed to appear has just appeared" ;
-       'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC;
-       'sTR"report this error," ; 'sPC ;
-       'sTR"Or you are using a user-written tactic which calls" ; 'sPC ;
-       'sTR"generic__modify_opers, in which case the user-written code" ;
-       'sPC ; 'sTR"is broken - this function is an internal system" ;
-       'sPC ; 'sTR"for internal system use only" >]
+    (str"An oper which was never supposed to appear has just appeared" ++
+     spc () ++ str"Either this is in system code, and you need to" ++ spc () ++
+     str"report this error," ++ spc () ++
+     str"Or you are using a user-written tactic which calls" ++ spc () ++
+     str"generic__modify_opers, in which case the user-written code" ++
+     spc () ++ str"is broken - this function is an internal system" ++
+     spc () ++ str"for internal system use only")
 
 let modify_opers replfun (constl,indl,cstrl) =
   let rec substrec c =
@@ -101,11 +101,11 @@ let expmod_constr modlist c =
   let expfun (sp,cb) = 
     if cb.const_opaque then
       errorlabstrm "expmod_constr"
-	[< 'sTR"Cannot unfold the value of ";
-        'sTR(string_of_path sp); 'sPC;
-        'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
-        'sTR"and then require that theorems which use them"; 'sPC;
-        'sTR"be transparent" >];
+	(str"Cannot unfold the value of " ++
+        str(string_of_path sp) ++ spc () ++
+        str"You cannot declare local lemmas as being opaque" ++ spc () ++
+        str"and then require that theorems which use them" ++ spc () ++
+        str"be transparent");
     match cb.const_body with
       | Some body -> body
       | None -> assert false
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e03d489c7f..0d341aabc4 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -82,13 +82,13 @@ let reset_rel_context env =
 let fold_named_context f env ~init =
   snd (Sign.fold_named_context
 	 (fun d (env,e) -> (push_named_decl d env, f env d e))
-         (named_context env) (reset_context env,init))
+         (named_context env) ~init:(reset_context env,init))
 
-let fold_named_context_reverse f a env =
-  Sign.fold_named_context_reverse f a (named_context env) 
+let fold_named_context_reverse f ~init env =
+  Sign.fold_named_context_reverse f ~init:init (named_context env) 
 
 let push_rel d   = rel_context_app (add_rel_decl d)
-let push_rel_context ctxt = fold_rel_context push_rel ctxt
+let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
 let push_rel_assum (id,ty) = push_rel (id,None,ty)
 
 let push_rec_types (lna,typarray,_) env =
@@ -100,7 +100,7 @@ let push_rec_types (lna,typarray,_) env =
 let fold_rel_context f env ~init =
   snd (fold_rel_context
 	 (fun d (env,e) -> (push_rel d env, f env d e))
-         (rel_context env) (reset_rel_context env,init))
+         (rel_context env) ~init:(reset_rel_context env,init))
 
 let set_universes g env =
   if env.env_universes == g then env else { env with env_universes = g }
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 218edd3a46..395ec95de2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -97,7 +97,8 @@ let instantiate_params t args sign =
           | (Some b,_,LetIn(_,_,_,t))    -> (largs, (substl subs b)::subs, t)
 	  | _                            -> fail())
       sign
-      (args,[],t) in
+      ~init:(args,[],t) 
+  in
   if rem_args <> [] then fail();
   type_app (substl subs) ty
 
@@ -190,8 +191,9 @@ let local_rels ctxt =
         match copt with
             None   -> (mkRel n :: rels, n+1)
           | Some _ -> (rels, n+1))
-      ([],1)
-      ctxt in
+      ~init:([],1)
+      ctxt 
+  in
   rels
 
 let build_dependent_constructor cs =
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 83474f1227..20bd1e03a6 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -40,8 +40,8 @@ let instance_from_named_context sign =
     | [] -> [] in
   Array.of_list (inst_rec sign)
 
-let fold_named_context = List.fold_right
-let fold_named_context_reverse = List.fold_left
+let fold_named_context f l ~init = List.fold_right f l init
+let fold_named_context_reverse f ~init l = List.fold_left f init l
 
 (*s Signatures of ordered section variables *)
 type section_context = named_context
@@ -66,8 +66,8 @@ let lookup_rel n sign =
 
 let rel_context_length = List.length
 
-let fold_rel_context = List.fold_right
-let fold_rel_context_reverse = List.fold_left
+let fold_rel_context f l ~init:x = List.fold_right f l x
+let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
 
 (* Push named declarations on top of a rel context *)
 (* Bizarre. Should be avoided. *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 8c7d7ccd08..16524ea469 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1020,7 +1020,7 @@ let rec to_lambda n prod =
     match kind_of_term prod with 
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
       | Cast (c,_) -> to_lambda n c
-      | _   -> errorlabstrm "to_lambda" [<>]                      
+      | _   -> errorlabstrm "to_lambda" (mt ())                      
 
 let rec to_prod n lam =
   if n=0 then 
@@ -1029,7 +1029,7 @@ let rec to_prod n lam =
     match kind_of_term lam with 
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
       | Cast (c,_) -> to_prod n c
-      | _   -> errorlabstrm "to_prod" [<>]                      
+      | _   -> errorlabstrm "to_prod" (mt ())                      
 	    
 (* pseudo-reduction rule:
  * [prod_app  s (Prod(_,B)) N --> B[N]
@@ -1040,7 +1040,7 @@ let prod_app t n =
     | Prod (_,_,b) -> subst1 n b
     | _ ->
 	errorlabstrm "prod_app"
-	  [< 'sTR"Needed a product, but didn't find one" ; 'fNL >]
+	  (str"Needed a product, but didn't find one" ++ fnl ())
 
 
 (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6556b0c764..ce62acdf8f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -103,7 +103,7 @@ let rec check_hyps_inclusion env sign =
       if not (eq_constr ty2 ty1) then
         error "types do not match")
     sign
-    ()
+    ~init:()
 
 
 let check_args env c hyps =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 99dd2ee361..c5b9983801 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -49,23 +49,25 @@ let string_of_univ = function
 	 ((List.map string_of_univ_level gel)@
 	  (List.map (fun u -> "("^(string_of_univ_level u)^")+1") gtl)))^")"
 
-let pr_uni_level u = [< 'sTR (string_of_univ_level u) >]
+let pr_uni_level u = str (string_of_univ_level u)
 
 let pr_uni = function
-  | Variable u -> pr_uni_level u
+  | Variable u -> 
+      pr_uni_level u
   | Max (gel,gtl) ->
-      [< 'sTR "max("; 
-	 prlist_with_sep pr_coma pr_uni_level gel;
-	 if gel <> [] & gtl <> [] then pr_coma () else [< >];
-	 prlist_with_sep pr_coma
-	   (fun x -> [< 'sTR "("; pr_uni_level x; 'sTR")+1" >]) gtl;
-	 'sTR ")" >]
+      str "max(" ++ 
+      prlist_with_sep pr_coma pr_uni_level gel ++
+      if gel <> [] & gtl <> [] then pr_coma () else mt () ++
+      prlist_with_sep pr_coma
+	(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++
+      str ")"
 
 (* Returns a fresh universe, juste above u. Does not create new universes
    for Type_0 (the sort of Prop and Set).
    Used to type the sort u. *)
 let super = function
-  | Variable u -> Max ([],[u])
+  | Variable u -> 
+      Max ([],[u])
   | Max _ ->
       anomaly ("Cannot take the successor of a non variable universes:\n"^
        "you are probably typing a type already known to be the type\n"^
@@ -125,7 +127,7 @@ let repr g u =
     let a =
       try UniverseMap.find u g
       with Not_found -> anomalylabstrm "Univ.repr"
-	  [< 'sTR"Universe "; pr_uni_level u; 'sTR" undefined" >] 
+	  (str"Universe " ++ pr_uni_level u ++ str" undefined") 
     in
     match a with 
       | Equiv(_,v) -> repr_rec v
@@ -405,13 +407,12 @@ let num_edges g =
     
 let pr_arc = function 
   | Canonical {univ=u; gt=gt; ge=ge} -> 
-      hOV 2
-        [< pr_uni_level u; 'sPC;
-           prlist_with_sep pr_spc (fun v -> [< 'sTR">"; pr_uni_level v >]) gt;
-           prlist_with_sep pr_spc (fun v -> [< 'sTR">="; pr_uni_level v >]) ge
-        >]
+      hov 2
+        (pr_uni_level u ++ spc () ++
+         prlist_with_sep pr_spc (fun v -> str ">" ++ pr_uni_level v) gt ++
+         prlist_with_sep pr_spc (fun v -> str ">=" ++ pr_uni_level v) ge)
   | Equiv (u,v) -> 
-      [< pr_uni_level u ; 'sTR"=" ; pr_uni_level v >]
+      pr_uni_level u  ++ str "=" ++ pr_uni_level v
 
 let pr_universes g =
   let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in