MAJ ocaml 2.99 (espaces dans la syntaxe des cast)

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

2 files changed, 9 insertions, 9 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index ec23d32585..ec7b8d4f76 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -74,12 +74,12 @@ let restore_decl sp evd evc =
  *
  * It is an error to cause SP to change state while we are focused on it. *)
 
-let w_Focusing_THEN sp (wt:'a result_w_tactic) (wt':'a -> w_tactic)
-                       (wc:walking_constraints) =
+let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
+                       (wc : walking_constraints) =
   let focus = (ts_it (ids_it wc)).focus
   and env  = (ts_it (ids_it wc)).env
   and evd   = Evd.map (ts_it (ids_it wc)).decls sp in
-  let (wc':walking_constraints) = ids_mod (extract_decl sp) wc in
+  let (wc' : walking_constraints) = ids_mod (extract_decl sp) wc in
   let (wc'',rslt) = wt wc' in 
   if not (ids_eq wc wc'') then error "w_saving_focus";
   if ts_eq (ids_it wc') (ids_it wc'') then 
@@ -94,7 +94,7 @@ let w_Focusing_THEN sp (wt:'a result_w_tactic) (wt':'a -> w_tactic)
                       decls = evc.decls }))
          wc''')
       
-let w_add_sign (id,t) (wc:walking_constraints) =
+let w_add_sign (id,t) (wc : walking_constraints) =
   ids_mk (ts_mod
             (fun evr ->
                { focus = evr.focus;
@@ -118,7 +118,7 @@ let w_hyps    wc    = var_context (get_env (ids_it wc))
 let w_ORELSE wt1 wt2 wc = 
   try wt1 wc with e when catchable_exception e -> wt2 wc
 
-let w_Declare sp c (wc:walking_constraints) =
+let w_Declare sp c (wc : walking_constraints) =
   begin match c with 
     | DOP2(Cast,_,_) -> ()
     | _ -> error "Cannot declare an un-casted evar"
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3c8e390584..c5e77abfba 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -71,7 +71,7 @@ let rec norm_evar_pf sigma p =
    [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ;
    (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] *)
 
-let rec mapshape nl (fl:(proof_tree list -> proof_tree) list) 
+let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) 
                     (l : proof_tree list) =
   match nl with
     | [] -> []
@@ -398,7 +398,7 @@ let tclTHENSI tac1 tac2l = tclTHENSi tac1 tac2l (fun _ -> tclIDTAC);;
 
 (* tclTHENL tac1 tac2 gls applies the tactic tac1 to gls and tac2
    to the last resulting subgoal *)
-let tclTHENL (tac1:tactic) (tac2:tactic) (gls:goal sigma) =
+let tclTHENL (tac1 : tactic) (tac2 : tactic) (gls : goal sigma) =
   finish_tac (theni_tac (-1) tac2 (then_tac tac1 (start_tac gls)))
 ;;
 
@@ -445,7 +445,7 @@ let tclWEAK_PROGRESS tac ptree =
 
 (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
    one of them being identical to the original goal *)
-let tclNOTSAMEGOAL (tac:tactic) goal =
+let tclNOTSAMEGOAL (tac : tactic) goal =
   let rslt = tac goal in
   let gls = (fst rslt).it in
   if List.exists (same_goal goal.it) gls
@@ -896,7 +896,7 @@ let print_subscript sigma sign pf =
   else 
     format_print_info_script sigma sign pf
 
-let tclINFO (tac:tactic) gls = 
+let tclINFO (tac : tactic) gls = 
   let (sgl,v) as res = tac gls in 
   begin try 
     let pf = v (List.map leaf (sig_it sgl)) in