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

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 9b1f57484b..7524c72a64 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -20,7 +20,7 @@ open Evarutil
 
 (* An auxiliary function for searching for fixpoint guard indexes *)
 
-val search_guard : 
+val search_guard :
     Util.loc -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types option | IsType
@@ -28,56 +28,56 @@ type typing_constraint = OfType of types option | IsType
 type var_map = (identifier * unsafe_judgment) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 
-module type S = 
+module type S =
 sig
 
   module Cases : Cases.S
-    
+
   (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   val allow_anonymous_refs : bool ref
 
   (* Generic call to the interpreter from rawconstr to open_constr, leaving
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
-  
+
   val understand_tcc : ?resolve_classes:bool ->
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
-    
+
   val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
     evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
 
   (* More general entry point with evars from ltac *)
-    
+
   (* Generic call to the interpreter from rawconstr to constr, failing
      unresolved holes in the rawterm cannot be instantiated.
-     
+
      In [understand_ltac sigma env ltac_env constraint c],
-     
+
      sigma : initial set of existential variables (typically dependent subgoals)
      ltac_env : partial substitution of variables (used for the tactic language)
-     constraint : tell if interpreted as a possibly constrained term or a type 
+     constraint : tell if interpreted as a possibly constrained term or a type
   *)
-    
+
   val understand_ltac :
     evar_map -> env -> var_map * unbound_ltac_var_map ->
     typing_constraint -> rawconstr -> evar_defs * constr
-    
+
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
-    
+
   val understand : evar_map -> env -> ?expected_type:Term.types ->
     rawconstr -> constr
-    
+
   (* Idem but the rawconstr is intended to be a type *)
-    
+
   val understand_type : evar_map -> env -> rawconstr -> constr
-    
+
   (* A generalization of the two previous case *)
-    
-  val understand_gen : typing_constraint -> evar_map -> env -> 
+
+  val understand_gen : typing_constraint -> evar_map -> env ->
     rawconstr -> constr
-    
+
   (* Idem but returns the judgment of the understood term *)
-    
+
   val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
   (* Idem but do not fail on unresolved evars *)
@@ -86,12 +86,12 @@ sig
   (*i*)
   (* Internal of Pretyping...
    *)
-  val pretype : 
-    type_constraint -> env -> evar_defs ref -> 
+  val pretype :
+    type_constraint -> env -> evar_defs ref ->
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_judgment
-    
-  val pretype_type : 
+
+  val pretype_type :
     val_constraint -> env -> evar_defs ref ->
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_type_judgment
@@ -102,17 +102,17 @@ sig
     typing_constraint -> rawconstr -> constr
 
   (*i*)
-    
+
 end
 
 module Pretyping_F (C : Coercion.S) : S
 module Default : S
 
 (* To embed constr in rawconstr *)
-  
+
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr
 
-val interp_sort : rawsort -> sorts  
+val interp_sort : rawsort -> sorts
 val interp_elimination_sort : rawsort -> sorts_family