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, 25 insertions, 25 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index 4bdbeee66..2d5ff3e43 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -71,17 +71,17 @@ let push_rel d env =
       env_rel_context = d :: env.env_rel_context }
 
 let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
-    
+
 let push_rec_types (lna,typarray,_) env =
   let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 (* Named context *)
 
-let push_named d env = 
+let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
   assert (env.env_rel_context = []); *)
-    { env with  
+    { env with
       env_named_context = d :: env.env_named_context }
 
 let lookup_named id env =
@@ -98,11 +98,11 @@ let named_type id env =
 
 (* Universe constraints *)
 let add_constraints c env =
-  if c == Constraint.empty then 
-    env 
+  if c == Constraint.empty then
+    env
   else
     let s = env.env_stratification in
-    { env with env_stratification = 
+    { env with env_stratification =
       { s with env_universes = merge_constraints c s.env_universes } }
 
 (* Global constants *)
@@ -111,17 +111,17 @@ let lookup_constant kn env =
   Cmap.find kn env.env_globals.env_constants
 
 let add_constant kn cs env =
-  let new_constants = 
+  let new_constants =
     Cmap.add kn cs env.env_globals.env_constants in
-  let new_globals = 
-    { env.env_globals with 
-	env_constants = new_constants } in 
+  let new_globals =
+    { env.env_globals with
+	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
 (* constant_type gives the type of a constant *)
 let constant_type env kn =
   let cb = lookup_constant kn env in
-  cb.const_type  
+  cb.const_type
 
 type const_evaluation_result = NoBody | Opaque
 
@@ -147,15 +147,15 @@ let evaluable_constant cst env =
 let lookup_mind kn env =
   KNmap.find kn env.env_globals.env_inductives
 
-let rec scrape_mind env kn = 
+let rec scrape_mind env kn =
   match (lookup_mind kn env).mind_equiv with
     | None -> kn
     | Some kn' -> scrape_mind env kn'
 
 let add_mind kn mib env =
   let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
-  let new_globals = 
-    { env.env_globals with 
+  let new_globals =
+    { env.env_globals with
 	env_inductives = new_inds } in
   { env with env_globals = new_globals }
 
@@ -168,36 +168,36 @@ let rec mind_equiv env (kn1,i1) (kn2,i2) =
 
 (* Modules *)
 
-let add_modtype ln mtb env = 
+let add_modtype ln mtb env =
   let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
-  let new_globals = 
-    { env.env_globals with 
+  let new_globals =
+    { env.env_globals with
 	env_modtypes = new_modtypes } in
   { env with env_globals = new_globals }
 
-let shallow_add_module mp mb env = 
+let shallow_add_module mp mb env =
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
-  let new_globals = 
-    { env.env_globals with 
+  let new_globals =
+    { env.env_globals with
 	env_modules = new_mods } in
   { env with env_globals = new_globals }
 
 let register_alias mp1 mp2 env =
   let new_alias =  MPmap.add mp1 mp2 env.env_globals.env_alias in
-  let new_globals = 
-    { env.env_globals with 
+  let new_globals =
+    { env.env_globals with
 	env_alias = new_alias } in
     { env with env_globals = new_globals }
 
-let rec scrape_alias mp env = 
+let rec scrape_alias mp env =
   try
     let mp1 = MPmap.find mp env.env_globals.env_alias in
       scrape_alias mp1 env
   with
       Not_found -> mp
 
-let lookup_module mp env = 
+let lookup_module mp env =
   MPmap.find mp env.env_globals.env_modules
 
-let lookup_modtype ln env = 
+let lookup_modtype ln env =
   MPmap.find ln env.env_globals.env_modtypes