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

11 files changed, 25 insertions, 25 deletions

diff --git a/kernel/sign.mli b/kernel/sign.mli
index 1970285895..fa05df814a 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -9,7 +9,7 @@ open Term
 
 (* Signatures of named variables. *)
 
-type 'a signature
+type 'a signature (* = identifier list * 'a list*)
 
 val nil_sign : 'a signature
 val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
diff --git a/kernel/term.ml b/kernel/term.ml
index a7ec0cfa1a..c08bb1d86e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1112,7 +1112,7 @@ let rec rename_bound_var l = function
 
 (* First utilities for avoiding telescope computation for subst_term *)
 
-let prefix_application k (c:constr) (t:constr) = 
+let prefix_application k (c : constr) (t : constr) = 
   match (whd_castapp c,whd_castapp t) with
     | ((DOPN(AppL,cl1)),DOPN(AppL,cl2)) ->
 	let l1 = Array.length cl1
@@ -1124,7 +1124,7 @@ let prefix_application k (c:constr) (t:constr) =
 	  None
     | (_,_) -> None
 
-let prefix_application_eta k (c:constr) (t:constr) = 
+let prefix_application_eta k (c : constr) (t : constr) = 
   match (whd_castapp c,whd_castapp t) with
     | ((DOPN(AppL,cl1)),DOPN(AppL,cl2)) ->
 	let l1 = Array.length cl1
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index c7931553bb..166d43536c 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -10,7 +10,7 @@ open Extend
 
 (* State of the grammar extensions *)
 
-let (grammar_state: grammar_command list ref) = ref []
+let (grammar_state : grammar_command list ref) = ref []
 
 (* Interpretation of the right hand side of grammar rules *)
 
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 86f5981feb..ab1aef1f5d 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -338,7 +338,7 @@ let list_filter_vec f vec =
    and the constr term that represent its type. *)
 
 let print_constructors_head 
-  (fn:string -> unit assumptions -> constr -> unit) c mip = 
+  (fn : string -> unit assumptions -> constr -> unit) c mip = 
   let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = array_map2 (fun id c_0 -> (id,c_0)) mip.mind_consnames lC in
@@ -360,7 +360,7 @@ let print_constructors_rel fn mip =
   let flid = list_filter_vec (fun (_,c) -> isRel (head_const c)) lidC in
   List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid
 
-let crible (fn:string -> unit assumptions -> constr -> unit) name =
+let crible (fn : string -> unit assumptions -> constr -> unit) name =
   let hyps = gLOB (Global.var_context()) in
   let imported = Library.opened_modules() in
   let const = global_reference CCI name in 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 911df0a8aa..fe78306208 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -82,7 +82,7 @@ let add_new_objdef (o,c,la,lp,l) =
     Lib.add_anonymous_leaf
       (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
 
-let ((inObjDef1:section_path -> obj),(outObjDef1:obj -> section_path)) =
+let ((inObjDef1 : section_path -> obj),(outObjDef1 : obj -> section_path)) =
   declare_object ("OBJDEF1",
                   { load_function = (fun _ -> ());
 		    open_function = (fun _ -> ());
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
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";