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

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 3583c8448..06f3291fe 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -24,13 +24,13 @@ let get_name avoid ?(default="H") = function
   | Name n -> Name n
 
 let array_get_start a =
-  try 
+  try
     Array.init
       (Array.length a - 1)
       (fun i -> a.(i))
-  with Invalid_argument "index out of bounds" -> 
+  with Invalid_argument "index out of bounds" ->
     invalid_argument "array_get_start"
-      
+
 let id_of_name = function
     Name id -> id
   | _ -> raise Not_found
@@ -78,7 +78,7 @@ let chop_rlambda_n  =
 	match rt with
 	  | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
 	  | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
-	  | _ -> 
+	  | _ ->
 	      raise (Util.UserError("chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
   in
@@ -107,11 +107,11 @@ let list_union_eq eq_fun l1 l2 =
 let list_add_set_eq eq_fun x l =
   if List.exists (eq_fun x) l then l else x::l
 
-  
+
 
 
 let const_of_id id =
-  let _,princ_ref = 
+  let _,princ_ref =
     qualid_of_reference (Libnames.Ident (Util.dummy_loc,id))
   in
   try Nametab.locate_constant princ_ref
@@ -119,7 +119,7 @@ let const_of_id id =
 
 let def_of_const t =
    match (Term.kind_of_term t) with
-    Term.Const sp -> 
+    Term.Const sp ->
       (try (match (Global.lookup_constant sp) with
              {Declarations.const_body=Some c} -> Declarations.force c
 	     |_ -> assert false)
@@ -127,17 +127,17 @@ let def_of_const t =
     |_ -> assert false
 
 let coq_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition" 
+  Coqlib.gen_constant_in_modules "RecursiveDefinition"
     (Coqlib.init_modules @ Coqlib.arith_modules) s;;
 
 let constant sl s =
   constr_of_global
-    (Nametab.locate (make_qualid(Names.make_dirpath 
+    (Nametab.locate (make_qualid(Names.make_dirpath
 			   (List.map id_of_string (List.rev sl)))
 	       (id_of_string s)));;
 
 let find_reference sl s =
-    (Nametab.locate (make_qualid(Names.make_dirpath 
+    (Nametab.locate (make_qualid(Names.make_dirpath
 			   (List.map id_of_string (List.rev sl)))
 	       (id_of_string s)));;
 
@@ -146,7 +146,7 @@ let refl_equal = lazy(coq_constant "refl_equal")
 
 (*****************************************************************)
 (* Copy of the standart save mechanism but without the much too  *)
-(* slow reduction function                                       *) 
+(* slow reduction function                                       *)
 (*****************************************************************)
 open Declarations
 open Entries
@@ -183,7 +183,7 @@ let save with_clean id const (locality,kind) hook =
 
 let extract_pftreestate pts =
   let pfterm,subgoals = Refiner.extract_open_pftreestate pts in
-  let tpfsigma = Refiner.evc_of_pftreestate pts in 
+  let tpfsigma = Refiner.evc_of_pftreestate pts in
   let exl = Evarutil.non_instantiated tpfsigma  in
   if subgoals <> [] or exl <> [] then
     Util.errorlabstrm "extract_proof"
@@ -198,19 +198,19 @@ let extract_pftreestate pts =
 let nf_betaiotazeta =
   let clos_norm_flags flgs env sigma t =
     Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiotazeta  
+  clos_norm_flags Closure.betaiotazeta
 
 let nf_betaiota =
   let clos_norm_flags flgs env sigma t =
     Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiota  
+  clos_norm_flags Closure.betaiota
 
 let cook_proof do_reduce =
-  let pfs = Pfedit.get_pftreestate () 
+  let pfs = Pfedit.get_pftreestate ()
 (*   and ident = Pfedit.get_current_proof_name ()  *)
   and (ident,strength,concl,hook) = Pfedit.current_proof_statement ()  in
   let env,sigma,pfterm = extract_pftreestate pfs in
-  let pfterm = 
+  let pfterm =
     if do_reduce
     then nf_betaiota env sigma pfterm
     else pfterm
@@ -228,32 +228,32 @@ let new_save_named opacity =
   let const = { const with const_entry_opaque = opacity } in
   save true id const persistence hook
 
-let get_proof_clean do_reduce = 
-  let result = cook_proof do_reduce in 
+let get_proof_clean do_reduce =
+  let result = cook_proof do_reduce in
   Pfedit.delete_current_proof ();
   result
 
-let with_full_print f a = 
+let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
-  let old_rawprint = !Flags.raw_print in 
+  let old_rawprint = !Flags.raw_print in
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
   Impargs.make_contextual_implicit_args false;
   Impargs.make_contextual_implicit_args false;
   Dumpglob.pause ();
-  try 
-    let res = f a in 
+  try
+    let res = f a in
     Impargs.make_implicit_args old_implicit_args;
     Impargs.make_strict_implicit_args old_strict_implicit_args;
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
     Dumpglob.continue ();
     res
-  with  
-    | e -> 
+  with
+    | e ->
 	Impargs.make_implicit_args old_implicit_args;
 	Impargs.make_strict_implicit_args old_strict_implicit_args;
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
@@ -268,19 +268,19 @@ let with_full_print f a =
 
 (**********************)
 
-type function_info = 
-    { 
+type function_info =
+    {
       function_constant : constant;
       graph_ind : inductive;
       equation_lemma : constant option;
       correctness_lemma : constant option;
-      completeness_lemma : constant option; 
+      completeness_lemma : constant option;
       rect_lemma : constant option;
       rec_lemma : constant option;
       prop_lemma : constant option;
       is_general : bool; (* Has this function been defined using general recursive definition *)
     }
-      
+
 
 (* type function_db  = function_info list *)
 
@@ -290,54 +290,54 @@ type function_info =
 let from_function = ref Cmap.empty
 let from_graph = ref Indmap.empty
 (*
-let rec do_cache_info finfo = function 
-  | [] -> raise Not_found 
-  | (finfo'::finfos as l) -> 
-      if finfo' == finfo then l 
-      else if finfo'.function_constant = finfo.function_constant 
+let rec do_cache_info finfo = function
+  | [] -> raise Not_found
+  | (finfo'::finfos as l) ->
+      if finfo' == finfo then l
+      else if finfo'.function_constant = finfo.function_constant
       then finfo::finfos
       else
-	let res = do_cache_info finfo finfos in 
+	let res = do_cache_info finfo finfos in
 	if res == finfos then l else  finfo'::l
-  
 
-let cache_Function (_,(finfos)) = 
-  let new_tbl = 
+
+let cache_Function (_,(finfos)) =
+  let new_tbl =
     try do_cache_info finfos !function_table
     with Not_found -> finfos::!function_table
-  in  
-  if new_tbl != !function_table 
+  in
+  if new_tbl != !function_table
   then function_table := new_tbl
 *)
 
-let cache_Function (_,finfos) = 
+let cache_Function (_,finfos) =
   from_function := Cmap.add finfos.function_constant finfos !from_function;
   from_graph := Indmap.add finfos.graph_ind finfos !from_graph
 
 
 let load_Function _  = cache_Function
 let open_Function _ = cache_Function
-let subst_Function (_,subst,finfos) = 
+let subst_Function (_,subst,finfos) =
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
   in
-  let function_constant' = do_subst_con finfos.function_constant in 
-  let graph_ind' = do_subst_ind finfos.graph_ind in 
-  let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in 
-  let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in 
-  let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in 
+  let function_constant' = do_subst_con finfos.function_constant in
+  let graph_ind' = do_subst_ind finfos.graph_ind in
+  let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
+  let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
+  let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
   let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
-  let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in 
-  let prop_lemma' =  Option.smartmap do_subst_con finfos.prop_lemma in 
-  if function_constant' == finfos.function_constant && 
-    graph_ind' == finfos.graph_ind && 
+  let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
+  let prop_lemma' =  Option.smartmap do_subst_con finfos.prop_lemma in
+  if function_constant' == finfos.function_constant &&
+    graph_ind' == finfos.graph_ind &&
     equation_lemma' == finfos.equation_lemma &&
-    correctness_lemma' == finfos.correctness_lemma && 
-    completeness_lemma' == finfos.completeness_lemma && 
-    rect_lemma' == finfos.rect_lemma && 
-    rec_lemma' == finfos.rec_lemma && 
-    prop_lemma' == finfos.prop_lemma 
-  then finfos 
+    correctness_lemma' == finfos.correctness_lemma &&
+    completeness_lemma' == finfos.completeness_lemma &&
+    rect_lemma' == finfos.rect_lemma &&
+    rec_lemma' == finfos.rec_lemma &&
+    prop_lemma' == finfos.prop_lemma
+  then finfos
   else
     { function_constant = function_constant';
       graph_ind = graph_ind';
@@ -355,25 +355,25 @@ let classify_Function infos = Libobject.Substitute infos
 let export_Function infos = Some infos
 
 
-let discharge_Function (_,finfos) = 
+let discharge_Function (_,finfos) =
   let function_constant' = Lib.discharge_con finfos.function_constant
-  and graph_ind' = Lib.discharge_inductive finfos.graph_ind 
-  and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma 
-  and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma 
-  and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma 
-  and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma 
+  and graph_ind' = Lib.discharge_inductive finfos.graph_ind
+  and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
+  and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
+  and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
+  and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
   and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
   and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
   in
-  if function_constant' == finfos.function_constant && 
-    graph_ind' == finfos.graph_ind && 
+  if function_constant' == finfos.function_constant &&
+    graph_ind' == finfos.graph_ind &&
     equation_lemma' == finfos.equation_lemma &&
-    correctness_lemma' == finfos.correctness_lemma && 
-    completeness_lemma' == finfos.completeness_lemma && 
-    rect_lemma' == finfos.rect_lemma && 
-    rec_lemma' == finfos.rec_lemma && 
-    prop_lemma' == finfos.prop_lemma 
-  then Some finfos 
+    correctness_lemma' == finfos.correctness_lemma &&
+    completeness_lemma' == finfos.completeness_lemma &&
+    rect_lemma' == finfos.rect_lemma &&
+    rec_lemma' == finfos.rec_lemma &&
+    prop_lemma' == finfos.prop_lemma
+  then Some finfos
   else
     Some { function_constant = function_constant' ;
 	   graph_ind = graph_ind' ;
@@ -384,12 +384,12 @@ let discharge_Function (_,finfos) =
 	   rec_lemma = rec_lemma';
 	   prop_lemma = prop_lemma' ;
 	   is_general = finfos.is_general
-	 }    
+	 }
 
 open Term
-let pr_info f_info = 
+let pr_info f_info =
   str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
-    str "function_constant_type := " ++ 
+    str "function_constant_type := " ++
     (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
     str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
     str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
@@ -397,15 +397,15 @@ let pr_info f_info =
     str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
     str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
     str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
-    str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () 
+    str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
 
-let pr_table tb = 
-  let l = Cmap.fold (fun k v acc -> v::acc) tb [] in 
+let pr_table tb =
+  let l = Cmap.fold (fun k v acc -> v::acc) tb [] in
   Util.prlist_with_sep fnl pr_info l
 
-let in_Function,out_Function = 
+let in_Function,out_Function =
   Libobject.declare_object
-    {(Libobject.default_object "FUNCTIONS_DB") with 
+    {(Libobject.default_object "FUNCTIONS_DB") with
        Libobject.cache_function = cache_Function;
        Libobject.load_function  = load_Function;
        Libobject.classify_function  = classify_Function;
@@ -418,57 +418,57 @@ let in_Function,out_Function =
 
 
 (* Synchronisation with reset *)
-let freeze () = 
+let freeze () =
   !from_function,!from_graph
-let unfreeze (functions,graphs) = 
+let unfreeze (functions,graphs) =
 (*   Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
   from_function := functions;
   from_graph := graphs
 
-let init () = 
+let init () =
 (*   Pp.msgnl (str "reseting function_table");  *)
   from_function := Cmap.empty;
   from_graph := Indmap.empty
 
-let _ = 
+let _ =
   Summary.declare_summary "functions_db_sum"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init }
 
-let find_or_none id = 
-  try Some 
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
-    ) 
+let find_or_none id =
+  try Some
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant"
+    )
   with Not_found -> None
 
 
 
-let find_Function_infos f = 
+let find_Function_infos f =
   Cmap.find f !from_function
 
 
-let find_Function_of_graph ind = 
+let find_Function_of_graph ind =
   Indmap.find ind !from_graph
-  
-let update_Function finfo = 
+
+let update_Function finfo =
 (*   Pp.msgnl (pr_info finfo); *)
   Lib.add_anonymous_leaf (in_Function finfo)
-      
-  
-let add_Function is_general f = 
-  let f_id = id_of_label (con_label f) in 
+
+
+let add_Function is_general f =
+  let f_id = id_of_label (con_label f) in
   let equation_lemma = find_or_none (mk_equation_id f_id)
-  and correctness_lemma = find_or_none (mk_correct_id f_id) 
-  and completeness_lemma = find_or_none (mk_complete_id f_id) 
+  and correctness_lemma = find_or_none (mk_correct_id f_id)
+  and completeness_lemma = find_or_none (mk_complete_id f_id)
   and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
   and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
-  and graph_ind = 
-    match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) 
+  and graph_ind =
+    match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
     with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
   in
-  let finfos = 
+  let finfos =
     { function_constant = f;
       equation_lemma = equation_lemma;
       completeness_lemma = completeness_lemma;
@@ -478,7 +478,7 @@ let add_Function is_general f =
       prop_lemma = prop_lemma;
       graph_ind = graph_ind;
       is_general = is_general
-      
+
     }
   in
   update_Function finfos
@@ -486,7 +486,7 @@ let add_Function is_general f =
 let pr_table () = pr_table !from_function
 (*********************************)
 (* Debuging *)
-let function_debug = ref false 
+let function_debug = ref false
 open Goptions
 
 let function_debug_sig =
@@ -501,13 +501,13 @@ let function_debug_sig =
 let _ = declare_bool_option function_debug_sig
 
 
-let do_observe () = 
+let do_observe () =
   !function_debug = true
-      
-      
-    
+
+
+
 let strict_tcc = ref false
-let is_strict_tcc () = !strict_tcc 
+let is_strict_tcc () = !strict_tcc
 let strict_tcc_sig =
   {
     optsync = false;
@@ -520,29 +520,29 @@ let strict_tcc_sig =
 let _ = declare_bool_option strict_tcc_sig
 
 
-exception Building_graph of exn 
+exception Building_graph of exn
 exception Defining_principle of exn
 exception ToShow of exn
 
-let init_constant dir s = 
-  try 
+let init_constant dir s =
+  try
     Coqlib.gen_constant "Function" dir s
   with e -> raise (ToShow e)
 
-let jmeq () =   
-  try 
-    (Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; 
+let jmeq () =
+  try
+    (Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
      init_constant ["Logic";"JMeq"] "JMeq")
   with e -> raise (ToShow e)
 
-let jmeq_rec () = 
+let jmeq_rec () =
   try
-    Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; 
+    Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
 	  init_constant ["Logic";"JMeq"] "JMeq_rec"
   with e -> raise (ToShow e)
 
-let jmeq_refl () = 
-  try 
+let jmeq_refl () =
+  try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
     init_constant ["Logic";"JMeq"] "JMeq_refl"
   with e -> raise (ToShow e)