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

4 files changed, 9 insertions, 9 deletions

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 1b47b7c1e4..5969cebbbb 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -191,8 +191,8 @@ let specification_dd x = x
 
 type destructor_data_object = identifier * destructor_data
 
-let ((inDD:destructor_data_object->obj),
-     (outDD:obj->destructor_data_object)) =
+let ((inDD : destructor_data_object->obj),
+     (outDD : obj->destructor_data_object)) =
   declare_object ("DESTRUCT-HYP-CONCL-DATA",
                   { load_function = (fun _ -> ());
                     cache_function = cache_dd;
@@ -306,7 +306,7 @@ let _ =
 		 | [] -> dConcl
 		 | _ -> bad_tactic_args "DConcl"))
 
-let to2Lists (table:t) = Nbtermdn.to2lists table
+let to2Lists (table : t) = Nbtermdn.to2lists table
 
 let rec search n =
   if n=0 then error "Search has reached zero.";
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 239b5e84f3..78fa139741 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -82,13 +82,13 @@ let dest_soapp_operator = function
       Some (n,list_uniquize [p])
   | _ -> None
 
-let constrain ((n:int),(m:constr)) sigma =
+let constrain ((n : int),(m : constr)) sigma =
   if List.mem_assoc n sigma then
     if eq_constr m (List.assoc n sigma) then sigma else error "somatch"
   else 
     (n,m)::sigma
     
-let build_dlam toabstract stk (m:constr) = 
+let build_dlam toabstract stk (m : constr) = 
   let rec buildrec m p_0 p_1 = match p_0,p_1 with 
     | (_, []) -> m
     | (n, (na::tl)) -> 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 7b4a9b2cf9..54d04def05 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -53,7 +53,7 @@ let tclTHEN_i1 tac1 tac2 = tclTHEN_i tac1 tac2 1
 
 (* apply a tactic to the nth element of the signature  *)
 
-let tclNTH_HYP m (tac:constr->tactic) gl =
+let tclNTH_HYP m (tac : constr->tactic) gl =
   tac (try VAR(fst(nth_sign (pf_untyped_hyps gl) m)) 
        with Failure _ -> error "No such assumption") gl
 
@@ -61,7 +61,7 @@ let tclNTH_HYP m (tac:constr->tactic) gl =
 
 let tclLAST_HYP = tclNTH_HYP 1
 
-let tclTRY_sign (tac:constr->tactic) sign gl =
+let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
     | []      -> tclFAIL
     | [s]     -> tac (VAR(s)) (* added in order to get useful error messages *)
@@ -69,7 +69,7 @@ let tclTRY_sign (tac:constr->tactic) sign gl =
   in 
   arec (ids_of_sign sign) gl
 
-let tclTRY_HYPS (tac:constr->tactic) gl = 
+let tclTRY_HYPS (tac : constr->tactic) gl = 
   tclTRY_sign tac (pf_untyped_hyps gl) gl
 
 (* OR-branch *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1997f09bba..b8cfc3b45a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -727,7 +727,7 @@ let dyn_exact cc gl = match cc with
       refine c gl 
   | l -> bad_tactic_args "exact" l 
 
-let (assumption:tactic) = fun gl ->
+let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
   let rec arec sign =
     if isnull_sign sign then error "No such assumption";