Corrections post contournement des streams avec ++

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

2 files changed, 14 insertions, 14 deletions

diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
index 47fc9929f7..cd5badbed6 100644
--- a/contrib/correctness/pextract.ml
+++ b/contrib/correctness/pextract.ml
@@ -54,7 +54,7 @@ let int_of_z = function
   | POS p -> int_of_pos p
   | NEG p -> -(int_of_pos p)
  ++ ++
-" >] (* '"' *)
+") (* '"' *)
 
 (* collect all section-path in a CIC constant *)
 
@@ -147,14 +147,14 @@ let rename_global 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
@@ -240,7 +240,7 @@ let pp_prog id =
 	   str" <-" ++ spc () ++ hov 2 (pp env rn false e2))
     | Seq bl ->
 	(str"begin" ++ fnl () ++
-	   str"  " ++ hov 0 (pp_block env rn bl ++) ++ 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) ++
@@ -256,15 +256,15 @@ let pp_prog id =
 			 None -> (mt ()) 
 		       | Some c -> (str"(* invariant: " ++ pTERM c.a_value ++ 
 				      str" *)" ++ fnl ())) ++
-		    pp_block env rn bl ++) ++ fnl () ++
-	   str"done" ++)
+		    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])
+    | 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 
@@ -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/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index c5294c0b70..55c45dd4d1 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -267,15 +267,15 @@ let explain_ml_case k ctx mes c ct br brt =
       | "Decomp" ->
           let plf = P.pr_term k ctx br in
           let pft = P.pr_term k ctx brt in
-          (str "The branch " ++ plf ++ 'wS 1 ++ cut () ++ str "has type " ++ pft ++
-             'wS 1 ++ cut () ++
+          (str "The branch " ++ plf ++ ws 1 ++ cut () ++ str "has type " ++ pft ++
+             ws 1 ++ cut () ++
              str "does not correspond to the inductive definition")
       | "Dependent" ->
           (str "ML case not allowed for a dependent case elimination")
       | _ -> (mt ())
   in
-  hov 0 (str "In ML case expression on " ++ pc ++ 'wS 1 ++ cut () ++
-           str "of type" ++  'wS 1 ++ pct ++ 'wS 1 ++ cut () ++ 
+  hov 0 (str "In ML case expression on " ++ pc ++ ws 1 ++ cut () ++
+           str "of type" ++  ws 1 ++ pct ++ ws 1 ++ cut () ++ 
            str "which is an inductive predicate." ++ fnl () ++ expln)
 (*
 let explain_cant_find_case_type loc k ctx c =
@@ -283,7 +283,7 @@ let explain_cant_find_case_type loc k ctx c =
   Ast.user_err_loc
     (loc,"pretype",
      hov 3 (str "Cannot infer type of whole Case expression on" ++ 
-	     'wS 1 ++ pe))
+	     ws 1 ++ pe))
 *)
 let explain_type_error k ctx = function
   | UnboundRel n ->