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

6 files changed, 60 insertions, 60 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index f9ca94ff6..f60abaf85 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -38,7 +38,7 @@ let glob_Ascii = lazy (make_reference "Ascii")
 open Lazy
 
 let interp_ascii dloc p =
-  let rec aux n p = 
+  let rec aux n p =
      if n = 0 then [] else
      let mp = p mod 2 in
      RRef (dloc,if mp = 0 then glob_false else glob_true)
@@ -46,7 +46,7 @@ let interp_ascii dloc p =
   RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p)
 
 let interp_ascii_string dloc s =
-  let p = 
+  let p =
     if String.length s = 1 then int_of_char s.[0]
     else
       if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2]
@@ -62,12 +62,12 @@ let uninterp_ascii r =
     | RRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
     | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
-  try 
+  try
     let rec aux = function
     | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
-  with 
+  with
    Non_closed_ascii -> None
 
 let make_ascii_string n =
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index c62c81377..5d20c2a3c 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -33,7 +33,7 @@ open Names
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
       if less_than (of_string "5000") n then
-	Flags.if_warn msg_warning 
+	Flags.if_warn msg_warning
 	  (strbrk "Stack overflow or segmentation fault happens when " ++
 	   strbrk "working with large numbers in nat (observed threshold " ++
 	   strbrk "may vary from 5000 to 70000 depending on your system " ++
@@ -41,11 +41,11 @@ let nat_of_int dloc n =
       let ref_O = RRef (dloc, glob_O) in
       let ref_S = RRef (dloc, glob_S) in
       let rec mk_nat acc n =
-	if n <> zero then 
+	if n <> zero then
 	  mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
-	else 
+	else
 	  acc
-      in 
+      in
       mk_nat ref_O n
     end
   else
@@ -61,9 +61,9 @@ let rec int_of_nat = function
   | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
   | RRef (_,z) when z = glob_O -> zero
   | _ -> raise Non_closed_number
-	  
+
 let uninterp_nat p =
-  try 
+  try
     Some (int_of_nat p)
   with
     Non_closed_number -> None
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 94e4c103a..e58618219 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -22,7 +22,7 @@ let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l))
 let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id)
 
 (* copied on g_zsyntax.ml, where it is said to be a temporary hack*)
-(* takes a path an identifier in the form of a string list and a string, 
+(* takes a path an identifier in the form of a string list and a string,
    returns a kernel_name *)
 let make_kn dir id = Libnames.encode_kn (make_dir dir) (Names.id_of_string id)
 
@@ -50,7 +50,7 @@ let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2)
 let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ]
 let bigN_path = make_path (bigN_module@["BigN"]) "t"
 (* big ugly hack *)
-let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), 
+let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)),
                              Names.mk_label "BigN")),
               [], Names.id_of_string id) : Names.kernel_name)
 let bigN_scope = "bigN_scope"
@@ -69,7 +69,7 @@ let bigN_constructor =
       else
 	2*(to_int quo)
   in
-  fun i -> 
+  fun i ->
   ConstructRef ((bigN_id "t_",0),
 		if less_than i n_inlined then
 		  (to_int i)+1
@@ -81,7 +81,7 @@ let bigN_constructor =
 let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ]
 let bigZ_path = make_path (bigZ_module@["BigZ"]) "t"
 (* big ugly hack bis *)
-let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), 
+let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)),
                              Names.mk_label "BigZ")),
               [], Names.id_of_string id) : Names.kernel_name)
 let bigZ_scope = "bigZ_scope"
@@ -108,7 +108,7 @@ exception Non_closed
 
 (* parses a *non-negative* integer (from bigint.ml) into an int31
    wraps modulo 2^31 *)
-let int31_of_pos_bigint dloc n = 
+let int31_of_pos_bigint dloc n =
   let ref_construct = RRef (dloc, int31_construct) in
   let ref_0 = RRef (dloc, int31_0) in
   let ref_1 = RRef (dloc, int31_1) in
@@ -124,7 +124,7 @@ let int31_of_pos_bigint dloc n =
 let error_negative dloc =
   Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
 
-let interp_int31 dloc n = 
+let interp_int31 dloc n =
   if is_pos_or_zero n then
     int31_of_pos_bigint dloc n
   else
@@ -132,20 +132,20 @@ let interp_int31 dloc n =
 
 (* Pretty prints an int31 *)
 
-let bigint_of_int31 = 
-  let rec args_parsing args cur = 
-    match args with 
+let bigint_of_int31 =
+  let rec args_parsing args cur =
+    match args with
       | [] -> cur
       | (RRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
       | (RRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur))
       | _ -> raise Non_closed
   in
-  function 
+  function
   | RApp (_, RRef (_, c), args) when c=int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
-let uninterp_int31 i = 
-  try 
+let uninterp_int31 i =
+  try
     Some (bigint_of_int31 i)
   with Non_closed ->
     None
@@ -169,12 +169,12 @@ let rank n = pow base (pow two n)
 (* splits a number bi at height n, that is the rest needs 2^n int31 to be stored
    it is expected to be used only when the quotient would also need 2^n int31 to be
    stored *)
-let split_at n bi = 
+let split_at n bi =
   euclid bi (rank (sub_1 n))
 
 (* search the height of the Coq bigint needed to represent the integer bi *)
 let height bi =
-  let rec height_aux n = 
+  let rec height_aux n =
     if less_than bi (rank n) then
       n
     else
@@ -199,7 +199,7 @@ let word_of_pos_bigint dloc hght n =
 			   decomp (sub_1 hgt) l])
   in
   decomp hght n
-      
+
 let bigN_of_pos_bigint dloc n =
   let ref_constructor i = RRef (dloc, bigN_constructor i) in
   let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then
@@ -210,11 +210,11 @@ let bigN_of_pos_bigint dloc n =
   in
   let hght = height n in
   result hght (word_of_pos_bigint dloc hght n)
-  
+
 let bigN_error_negative dloc =
   Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
 
-let interp_bigN dloc n = 
+let interp_bigN dloc n =
   if is_pos_or_zero n then
     bigN_of_pos_bigint dloc n
   else
@@ -223,13 +223,13 @@ let interp_bigN dloc n =
 
 (* Pretty prints a bigN *)
 
-let bigint_of_word = 
+let bigint_of_word =
   let rec get_height rc =
     match rc with
-    | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW -> 
+    | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
 	                                  let hleft = get_height lft in
 					  let hright = get_height rght in
-					  add_1 
+					  add_1
 					    (if less_than hleft hright then
 						 hright
 					     else
@@ -248,15 +248,15 @@ let bigint_of_word =
   fun rc ->
     let hght = get_height rc in
     transform hght rc
-    
+
 let bigint_of_bigN rc =
   match rc with
   | RApp (_,_,[one_arg]) -> bigint_of_word one_arg
   | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
   | _ -> raise Non_closed
 
-let uninterp_bigN rc = 
-  try 
+let uninterp_bigN rc =
+  try
     Some (bigint_of_bigN rc)
   with Non_closed ->
     None
@@ -266,7 +266,7 @@ let uninterp_bigN rc =
    numeral interpreter *)
 
 let bigN_list_of_constructors =
-  let rec build i = 
+  let rec build i =
     if less_than i (add_1 n_inlined) then
       RRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i))
     else
@@ -284,7 +284,7 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
 
 
 (*** Parsing for bigZ in digital notation ***)
-let interp_bigZ dloc n = 
+let interp_bigZ dloc n =
   let ref_pos = RRef (dloc, bigZ_pos) in
   let ref_neg = RRef (dloc, bigZ_neg) in
   if is_pos_or_zero n then
@@ -295,8 +295,8 @@ let interp_bigZ dloc n =
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
   | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
-  | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg -> 
-      let opp_val = bigint_of_bigN one_arg in 
+  | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg ->
+      let opp_val = bigint_of_bigN one_arg in
       if equal opp_val zero then
 	raise Non_closed
       else
@@ -304,8 +304,8 @@ let bigint_of_bigZ = function
   | _ -> raise Non_closed
 
 
-let uninterp_bigZ rc = 
-  try 
+let uninterp_bigZ rc =
+  try
     Some (bigint_of_bigZ rc)
   with Non_closed ->
     None
@@ -320,7 +320,7 @@ let _ = Notation.declare_numeral_interpreter bigZ_scope
    true)
 
 (*** Parsing for bigQ in digital notation ***)
-let interp_bigQ dloc n = 
+let interp_bigQ dloc n =
   let ref_z = RRef (dloc, bigQ_z) in
   let ref_pos = RRef (dloc, bigZ_pos) in
   let ref_neg = RRef (dloc, bigZ_neg) in
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 4a5972cc7..f85309e67 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -65,7 +65,7 @@ let r_of_posint dloc n =
 
 let r_of_int dloc z =
   if is_strictly_neg z then
-    RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) 
+    RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
   else
     r_of_posint dloc z
 
@@ -90,7 +90,7 @@ let rec bignat_of_pos = function
       mult_2 (bignat_of_pos b)
   (* 1+(1+1)*b *)
   | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])])
-      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  -> 
+      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  ->
       if bignat_of_pos a <> two then raise Non_closed_number;
         add_1 (mult_2 (bignat_of_pos b))
   | _ -> raise Non_closed_number
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index d1c263dc8..bc02357ae 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -38,14 +38,14 @@ open Lazy
 
 let interp_string dloc s =
   let le = String.length s in
-  let rec aux n = 
+  let rec aux n =
      if n = le then RRef (dloc, force glob_EmptyString) else
      RApp (dloc,RRef (dloc, force glob_String),
        [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
 let uninterp_string r =
-  try 
+  try
     let b = Buffer.create 16 in
     let rec aux = function
     | RApp (_,RRef (_,k),[a;s]) when k = force glob_String ->
@@ -57,13 +57,13 @@ let uninterp_string r =
     | _ ->
 	raise Non_closed_string
     in aux r
-  with 
+  with
    Non_closed_string -> None
 
 let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([RRef (dummy_loc,static_glob_String); 
+    ([RRef (dummy_loc,static_glob_String);
       RRef (dummy_loc,static_glob_EmptyString)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index bfbe54c28..a10c76013 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -33,7 +33,7 @@ let positive_path = make_path positive_module "positive"
 (* TODO: temporary hack *)
 let make_kn dir id = Libnames.encode_kn dir id
 
-let positive_kn = 
+let positive_kn =
   make_kn (make_dir positive_module) (id_of_string "positive")
 let glob_positive = IndRef (positive_kn,0)
 let path_of_xI = ((positive_kn,0),1)
@@ -52,10 +52,10 @@ let pos_of_bignat dloc x =
       | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
       | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q])
       | (q,true) -> ref_xH
-  in 
+  in
   pos_of x
 
-let error_non_positive dloc = 
+let error_non_positive dloc =
   user_err_loc (dloc, "interp_positive",
     str "Only strictly positive numbers in type \"positive\".")
 
@@ -74,9 +74,9 @@ let rec bignat_of_pos = function
   | _ -> raise Non_closed_number
 
 let uninterp_positive p =
-  try 
+  try
     Some (bignat_of_pos p)
-  with Non_closed_number -> 
+  with Non_closed_number ->
     None
 
 (************************************************************************)
@@ -87,7 +87,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,positive_module)
   interp_positive
   ([RRef (dummy_loc, glob_xI);
-    RRef (dummy_loc, glob_xO); 
+    RRef (dummy_loc, glob_xO);
     RRef (dummy_loc, glob_xH)],
    uninterp_positive,
    true)
@@ -106,10 +106,10 @@ let glob_Npos = ConstructRef path_of_Npos
 
 let n_path = make_path binnat_module "N"
 
-let n_of_binnat dloc pos_or_neg n = 
+let n_of_binnat dloc pos_or_neg n =
   if n <> zero then
     RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n])
-  else 
+  else
     RRef (dloc, glob_N0)
 
 let error_negative dloc =
@@ -138,11 +138,11 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnat_module)
   n_of_int
-  ([RRef (dummy_loc, glob_N0); 
+  ([RRef (dummy_loc, glob_N0);
     RRef (dummy_loc, glob_Npos)],
   uninterp_n,
   true)
-   
+
 (**********************************************************************)
 (* Parsing Z via scopes                                               *)
 (**********************************************************************)
@@ -158,12 +158,12 @@ let glob_ZERO = ConstructRef path_of_ZERO
 let glob_POS = ConstructRef path_of_POS
 let glob_NEG = ConstructRef path_of_NEG
 
-let z_of_int dloc n = 
+let z_of_int dloc n =
   if n <> zero then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
     RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
-  else 
+  else
     RRef (dloc, glob_ZERO)
 
 (**********************************************************************)
@@ -187,8 +187,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binint_module)
   z_of_int
-  ([RRef (dummy_loc, glob_ZERO); 
-    RRef (dummy_loc, glob_POS); 
+  ([RRef (dummy_loc, glob_ZERO);
+    RRef (dummy_loc, glob_POS);
     RRef (dummy_loc, glob_NEG)],
   uninterp_z,
   true)