Delete trailing whitespaces in all *.{v,ml*} files

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

1 files changed, 98 insertions, 98 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 97697f5de6..3f38cc2f7c 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -22,7 +22,7 @@ open Mod_subst
 
 
 
-let error_existing_label l = 
+let error_existing_label l =
   error ("The label "^string_of_label l^" is already declared.")
 
 let error_declaration_not_path _ = error "Declaration is not a path."
@@ -39,31 +39,31 @@ let error_not_match l _ = error ("Signature components for label "^string_of_lab
 
 let error_no_such_label l = error ("No such label "^string_of_label l^".")
 
-let error_incompatible_labels l l' = 
+let error_incompatible_labels l l' =
   error ("Opening and closing labels are not the same: "
 	 ^string_of_label l^" <> "^string_of_label l'^" !")
 
-let error_result_must_be_signature () = 
+let error_result_must_be_signature () =
   error "The result module type must be a signature."
 
 let error_signature_expected mtb =
   error "Signature expected."
 
-let error_no_module_to_end _ = 
+let error_no_module_to_end _ =
   error "No open module to end."
 
 let error_no_modtype_to_end _ =
   error "No open module type to end."
 
-let error_not_a_modtype_loc loc s = 
+let error_not_a_modtype_loc loc s =
   user_err_loc (loc,"",str ("\""^s^"\" is not a module type."))
 
-let error_not_a_module_loc loc s = 
+let error_not_a_module_loc loc s =
   user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
 
 let error_not_a_module s = error_not_a_module_loc dummy_loc s
 
-let error_not_a_constant l = 
+let error_not_a_constant l =
   error ("\""^(string_of_label l)^"\" is not a constant.")
 
 let error_with_incorrect l =
@@ -74,9 +74,9 @@ let error_a_generative_module_expected l =
          "component of generative modules can be changed using the \"with\" " ^
          "construct.")
 
-let error_local_context lo = 
+let error_local_context lo =
   match lo with
-      None -> 
+      None ->
 	error ("The local context is not empty.")
     | (Some l) ->
 	error ("The local context of the component "^
@@ -106,7 +106,7 @@ let destr_functor env mtb =
 
 (* the constraints are not important here *)
 
-let module_body_of_type mtb = 
+let module_body_of_type mtb =
   { mod_type = Some mtb.typ_expr;
     mod_expr = None;
     mod_constraints = Constraint.empty;
@@ -114,30 +114,30 @@ let module_body_of_type mtb =
     mod_retroknowledge = []}
 
 let module_type_of_module mp mb =
-  let mp1,expr = 
+  let mp1,expr =
       (match mb.mod_type with
 	| Some expr -> mp,expr
 	| None -> (match mb.mod_expr with
 		     | Some (SEBident mp') ->(Some mp'),(SEBident mp')
 		     | Some expr -> mp,expr
-		     | None -> 
+		     | None ->
 			 anomaly "Modops: empty expr and type")) in
     {typ_expr = expr;
       typ_alias = mb.mod_alias;
       typ_strength = mp1
     }
 
-let rec check_modpath_equiv env mp1 mp2 = 
+let rec check_modpath_equiv env mp1 mp2 =
   if mp1=mp2 then () else
   let mp1 = scrape_alias mp1 env in
   let mp2 = scrape_alias mp2 env in
     if mp1=mp2 then ()
-    else 
+    else
       error_not_equal mp1 mp2
-	
+
 let rec subst_with_body sub = function
   | With_module_body(id,mp,typ_opt,cst) ->
-      With_module_body(id,subst_mp sub mp,Option.smartmap 
+      With_module_body(id,subst_mp sub mp,Option.smartmap
 			 (subst_struct_expr sub) typ_opt,cst)
   | With_definition_body(id,cb) ->
       With_definition_body( id,subst_const_body sub cb)
@@ -148,22 +148,22 @@ and subst_modtype sub mtb =
     if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then
       mtb
     else
-      { mtb with 
+      { mtb with
 	  typ_expr = typ_expr';
 	  typ_alias = sub_mtb}
-	
-and subst_structure sub sign = 
+
+and subst_structure sub sign =
   let subst_body  = function
-      SFBconst cb -> 
+      SFBconst cb ->
 	SFBconst (subst_const_body sub cb)
-    | SFBmind mib -> 
+    | SFBmind mib ->
 	SFBmind (subst_mind sub mib)
-    | SFBmodule mb -> 
+    | SFBmodule mb ->
 	SFBmodule (subst_module sub mb)
-    | SFBmodtype mtb -> 
+    | SFBmodtype mtb ->
 	SFBmodtype (subst_modtype sub mtb)
     | SFBalias (mp,typ_opt,cst) ->
-	SFBalias (subst_mp sub mp,Option.smartmap 
+	SFBalias (subst_mp sub mp,Option.smartmap
 		    (subst_struct_expr sub) typ_opt,cst)
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
@@ -177,15 +177,15 @@ and subst_module  sub mb =
   let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in
   let mb_alias = update_subst sub mb.mod_alias in
    let mb_alias =  if mb_alias = empty_subst then
-     join_alias mb.mod_alias sub 
-   else 
+     join_alias mb.mod_alias sub
+   else
      join mb_alias (join_alias mb.mod_alias sub)
    in
-     if mtb'==mb.mod_type && mb.mod_expr == me' 
+     if mtb'==mb.mod_type && mb.mod_expr == me'
       && mb_alias == mb.mod_alias
     then mb else
       { mod_expr = me';
-	mod_type=mtb'; 
+	mod_type=mtb';
 	mod_constraints=mb.mod_constraints;
 	mod_alias = mb_alias;
 	mod_retroknowledge=mb.mod_retroknowledge}
@@ -193,7 +193,7 @@ and subst_module  sub mb =
 
 and subst_struct_expr sub = function
     | SEBident mp -> SEBident (subst_mp sub  mp)
-    | SEBfunctor (msid, mtb, meb') -> 
+    | SEBfunctor (msid, mtb, meb') ->
 	SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
     | SEBstruct (msid,str)->
 	SEBstruct(msid, subst_structure sub str)
@@ -201,15 +201,15 @@ and subst_struct_expr sub = function
 	SEBapply(subst_struct_expr sub meb1,
 		 subst_struct_expr sub meb2,
 		 cst)
-    | SEBwith (meb,wdb)-> 
+    | SEBwith (meb,wdb)->
 	SEBwith(subst_struct_expr sub meb,
 		subst_with_body sub wdb)
- 
 
-let subst_signature_msid msid mp = 
+
+let subst_signature_msid msid mp =
   subst_structure (map_msid msid mp)
 
-(* spiwack: here comes the function which takes care of importing 
+(* spiwack: here comes the function which takes care of importing
    the retroknowledge declared in the library *)
 (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
 let add_retroknowledge msid mp =
@@ -217,8 +217,8 @@ let add_retroknowledge msid mp =
   let subst_and_perform rkaction env =
     match rkaction with
       | Retroknowledge.RKRegister (f, e) ->
-	  Environ.register env f 
-	  (match e with 
+	  Environ.register env f
+	  (match e with
 	    | Const kn -> kind_of_term (subst_mps subst (mkConst kn))
 	    | Ind ind -> kind_of_term (subst_mps subst (mkInd ind))
 	    | _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term")
@@ -229,41 +229,41 @@ let add_retroknowledge msid mp =
      int31 type registration absolutely needs int31 bits to be registered.
      Since the local_retroknowledge is stored in reverse order (each new
      registration is added at the top of the list) we need a fold_right
-     for things to go right (the pun is not intented). So we lose 
+     for things to go right (the pun is not intented). So we lose
      tail recursivity, but the world will have exploded before any module
      imports 10 000 retroknowledge registration.*)
   List.fold_right subst_and_perform lclrk env
 
 
 
-let strengthen_const env mp l cb = 
+let strengthen_const env mp l cb =
   match cb.const_opaque, cb.const_body with
   | false, Some _ -> cb
-  | true, Some _ 
+  | true, Some _
   | _, None ->
-      let const = mkConst (make_con mp empty_dirpath l) in 
+      let const = mkConst (make_con mp empty_dirpath l) in
       let const_subs = Some (Declarations.from_val const) in
-	{cb with 
+	{cb with
 	   const_body = const_subs;
 	   const_opaque = false;
 	   const_body_code = Cemitcodes.from_val
             (compile_constant_body env const_subs false false)
 	}
-	  
+
 let strengthen_mind env mp l mib = match mib.mind_equiv with
   | Some _ -> mib
   | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
 
 
-let rec eval_struct env = function 
-  | SEBident mp -> 
+let rec eval_struct env = function
+  | SEBident mp ->
       begin
 	let mtb =lookup_modtype mp env in
 	match mtb.typ_expr,mtb.typ_strength with
 	    mtb,None -> eval_struct env mtb
 	  | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
       end
-  | SEBapply (seb1,seb2,_) -> 
+  | SEBapply (seb1,seb2,_) ->
       let svb1 = eval_struct env seb1 in
       let farg_id, farg_b, fbody_b = destr_functor env svb1 in
       let mp = path_of_seb seb2 in
@@ -271,15 +271,15 @@ let rec eval_struct env = function
       let sub_alias = (lookup_modtype mp env).typ_alias in
       let sub_alias = match eval_struct env (SEBident mp) with
 	| SEBstruct (msid,sign) ->
-	    join_alias 
+	    join_alias
 	      (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
        let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
-     let sub_alias1 = update_subst sub_alias 
+     let sub_alias1 = update_subst sub_alias
 	(map_mbid farg_id mp (Some resolve)) in
-	eval_struct env (subst_struct_expr 
-			   (join sub_alias1 
+	eval_struct env (subst_struct_expr
+			   (join sub_alias1
 			      (map_mbid farg_id mp (Some resolve))) fbody_b)
   | SEBwith (mtb,(With_definition_body _ as wdb)) ->
       let mtb',_ = merge_with env mtb wdb empty_subst in
@@ -292,24 +292,24 @@ let rec eval_struct env = function
 	| _ -> alias_in_mp in
       let mtb',_ = merge_with env mtb wdb alias_in_mp in
 	mtb'
-(*  | SEBfunctor(mbid,mtb,body) -> 
+(*  | SEBfunctor(mbid,mtb,body) ->
     let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
     SEBfunctor(mbid,mtb,eval_struct env body) *)
   | mtb -> mtb
-      
+
 and type_of_mb env mb =
   match mb.mod_type,mb.mod_expr with
       None,Some b -> eval_struct env b
     | Some t, _ -> eval_struct env t
-    | _,_ -> anomaly 
-	"Modops:  empty type and empty expr" 
-	  
-and merge_with env mtb with_decl alias= 
-  let msid,sig_b = match (eval_struct env mtb) with 
+    | _,_ -> anomaly
+	"Modops:  empty type and empty expr"
+
+and merge_with env mtb with_decl alias=
+  let msid,sig_b = match (eval_struct env mtb) with
     | SEBstruct(msid,sig_b) -> msid,sig_b
     | _ -> error_signature_expected mtb
   in
-  let id,idl = match with_decl with 
+  let id,idl = match with_decl with
     | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl
     | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
   in
@@ -320,20 +320,20 @@ and merge_with env mtb with_decl alias=
       let rec mp_rec = function
 	| [] -> MPself msid
 	| i::r -> MPdot(mp_rec r,label_of_id i)
-      in 
+      in
       let env' = add_signature (MPself msid) before env in
       let new_spec,subst = match with_decl with
         | With_definition_body ([],_)
         | With_module_body ([],_,_,_) -> assert false
-	| With_definition_body ([id],c) -> 
+	| With_definition_body ([id],c) ->
 	    SFBconst c,None
 	| With_module_body ([id], mp,typ_opt,cst) ->
 	    let mp' = scrape_alias mp env' in
 	    let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in
 	      SFBalias (mp,typ_opt,Some cst),
 	    Some(join (map_mp (mp_rec [id]) mp') new_alias)
-	| With_definition_body (_::_,_) 
-        | With_module_body (_::_,_,_,_) -> 
+	| With_definition_body (_::_,_)
+        | With_module_body (_::_,_,_,_) ->
 	    let old,aliasold = match spec with
 		SFBmodule msb -> Some msb, None
 	      | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst)
@@ -341,24 +341,24 @@ and merge_with env mtb with_decl alias=
 	    in
 	      if aliasold = None then
 		let old = Option.get old in
-		let new_with_decl,subst1 = 
+		let new_with_decl,subst1 =
 		  match with_decl with
                       With_definition_body (_,c) -> With_definition_body (idl,c),None
-		    | With_module_body (idc,mp,typ_opt,cst) -> 
+		    | With_module_body (idc,mp,typ_opt,cst) ->
 			let mp' = scrape_alias mp env' in
 			  With_module_body (idl,mp,typ_opt,cst),
-			Some(map_mp (mp_rec (List.rev idc)) mp') 
+			Some(map_mp (mp_rec (List.rev idc)) mp')
 		in
 		let subst = match subst1 with
 		  | None -> None
 		  | Some s -> Some (join s (update_subst alias s)) in
-		let modtype,subst_msb = 
+		let modtype,subst_msb =
 		  merge_with env' (type_of_mb env' old) new_with_decl alias in
 		let msb =
 		  { mod_expr = None;
-		    mod_type = Some modtype; 
+		    mod_type = Some modtype;
 		    mod_constraints = old.mod_constraints;
-		    mod_alias = begin 
+		    mod_alias = begin
 		      match subst_msb with
 			|None -> empty_subst
 			|Some s -> s
@@ -366,8 +366,8 @@ and merge_with env mtb with_decl alias=
 		    mod_retroknowledge = old.mod_retroknowledge}
 		in
 		  (SFBmodule msb),subst
-	      else 
-		let mpold,typ_opt,cst =  Option.get aliasold in 
+	      else
+		let mpold,typ_opt,cst =  Option.get aliasold in
 		  SFBalias (mpold,typ_opt,cst),None
       in
 	SEBstruct(msid,  before@(l,new_spec)::
@@ -375,36 +375,36 @@ and merge_with env mtb with_decl alias=
     with
 	Not_found -> error_no_such_label l
 
-and add_signature mp sign env = 
+and add_signature mp sign env =
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
     let con = make_con mp empty_dirpath l in
       match elem with
 	| SFBconst cb -> Environ.add_constant con cb env
 	| SFBmind mib -> Environ.add_mind kn mib env
-	| SFBmodule mb -> 
-	    add_module (MPdot (mp,l)) mb env 
+	| SFBmodule mb ->
+	    add_module (MPdot (mp,l)) mb env
 	      (* adds components as well *)
-	| SFBalias (mp1,_,cst) -> 
+	| SFBalias (mp1,_,cst) ->
 	    Environ.register_alias (MPdot(mp,l)) mp1 env
-	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) 
+	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l))
 	    mtb env
   in
     List.fold_left add_one env sign
 
-and add_module mp mb env = 
+and add_module mp mb env =
   let env = Environ.shallow_add_module mp mb env in
   let env =
     Environ.add_modtype mp (module_type_of_module (Some mp) mb) env
   in
   let mod_typ = type_of_mb env mb in
     match mod_typ with
-      | SEBstruct (msid,sign) -> 
+      | SEBstruct (msid,sign) ->
 	  add_retroknowledge msid mp (mb.mod_retroknowledge)
 	    (add_signature mp (subst_signature_msid msid mp sign) env)
       | SEBfunctor _ -> env
       | _ -> anomaly "Modops:the evaluation of the structure failed "
-	  
+
 
 
 and  constants_of_specification env mp sign =
@@ -413,30 +413,30 @@ and  constants_of_specification env mp sign =
    | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
    | SFBmind _ -> env,res
    | SFBmodule mb ->
-       let new_env =  add_module (MPdot (mp,l)) mb env in 
+       let new_env =  add_module (MPdot (mp,l)) mb env in
        new_env,(constants_of_modtype env (MPdot (mp,l))
 		   (type_of_mb env mb)) @ res
    | SFBalias (mp1,typ_opt,cst) ->
-       let new_env =  register_alias (MPdot (mp,l)) mp1 env in 
+       let new_env =  register_alias (MPdot (mp,l)) mp1 env in
        new_env,(constants_of_modtype env (MPdot (mp,l))
 		   (eval_struct env (SEBident mp1))) @ res
-   | SFBmodtype mtb -> 
-       (* module type dans un module type. 
-	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
-	  kn pour pouvoir continuer aller deplier les modules utilisant ce 
+   | SFBmodtype mtb ->
+       (* module type dans un module type.
+	  Il faut au moins mettre mtb dans l'environnement (avec le bon
+	  kn pour pouvoir continuer aller deplier les modules utilisant ce
 	  mtb
-	  ex: 
-	  Module Type T1. 
+	  ex:
+	  Module Type T1.
 	  Module Type T2.
 	     ....
     	    End T2.
 	  .....
             Declare Module M : T2.
-         End T2 
-	  si on ne rajoute pas T2 dans l'environement de typage 
+         End T2
+	  si on ne rajoute pas T2 dans l'environement de typage
 	  on va exploser au moment du Declare Module
        *)
-       let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in 
+       let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in
        new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res
  in
  snd (List.fold_left aux (env,[]) sign)
@@ -474,23 +474,23 @@ and  resolver_of_environment mbid modtype mp alias env =
  let resolve = make_resolve constants in
    Mod_subst.make_resolver resolve
 
-    
+
 and strengthen_mtb env mp mtb =
-  let mtb1 = eval_struct env mtb in 
+  let mtb1 = eval_struct env mtb in
   match  mtb1 with
   | SEBfunctor _ -> mtb1
-  | SEBstruct (msid,sign) -> 
+  | SEBstruct (msid,sign) ->
       SEBstruct (msid,strengthen_sig env msid sign mp)
   | _ -> anomaly "Modops:the evaluation of the structure failed "
 
-and strengthen_mod env mp mb = 
+and strengthen_mod env mp mb =
   let mod_typ = type_of_mb env mb in
     { mod_expr = mb.mod_expr;
       mod_type = Some (strengthen_mtb env mp mod_typ);
       mod_constraints = mb.mod_constraints;
       mod_alias = mb.mod_alias;
       mod_retroknowledge = mb.mod_retroknowledge}
-      
+
 and strengthen_sig env msid sign mp = match sign with
   | [] -> []
   | (l,SFBconst cb) :: rest ->
@@ -504,7 +504,7 @@ and strengthen_sig env msid sign mp = match sign with
   | (l,SFBmodule mb) :: rest ->
       let mp' = MPdot (mp,l) in
 	let item' = l,SFBmodule (strengthen_mod env mp' mb) in
-	let env' = add_module 
+	let env' = add_module
 	  (MPdot (MPself msid,l)) mb env in
         let rest' = strengthen_sig env' msid rest mp in
 	item':: rest'
@@ -512,22 +512,22 @@ and strengthen_sig env msid sign mp = match sign with
       let env' = register_alias (MPdot(MPself msid,l)) mp1 env in
       let rest' = strengthen_sig env' msid rest mp in
 	item::rest'
-  | (l,SFBmodtype mty as item) :: rest -> 
-      let env' = add_modtype 
-		   (MPdot((MPself msid),l)) 
+  | (l,SFBmodtype mty as item) :: rest ->
+      let env' = add_modtype
+		   (MPdot((MPself msid),l))
 		   mty
 		   env
       in
       let rest' = strengthen_sig env' msid rest mp in
 	item::rest'
 
-    
+
 let strengthen env mtb mp = strengthen_mtb env mp mtb
 
 
 let update_subst env mb mp =
   match type_of_mb env mb with
-    | SEBstruct(msid,str) -> false, join_alias 
+    | SEBstruct(msid,str) -> false, join_alias
 	(subst_key (map_msid msid mp) mb.mod_alias)
 	(map_msid msid mp)
     | _ -> true, mb.mod_alias