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

10 files changed, 82 insertions, 82 deletions

diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml
index 032ddbebe..40bc61bb8 100644
--- a/plugins/xml/acic.ml
+++ b/plugins/xml/acic.ml
@@ -56,7 +56,7 @@ type obj =
  | InductiveDefinition of
     inductiveType list *                           (* inductive types ,      *)
     params * int                                   (*  parameters,n ind. pars*)
-and inductiveType = 
+and inductiveType =
  identifier * bool * constr *                 (* typename, inductive, arity *)
   constructor list                            (*  constructors              *)
 and constructor =
@@ -78,9 +78,9 @@ type aconstr =
   | ACase      of id * uri * int * aconstr * aconstr * aconstr list
   | AFix       of id * int * ainductivefun list
   | ACoFix     of id * int * acoinductivefun list
-and ainductivefun = 
+and ainductivefun =
  id * identifier * int * aconstr * aconstr
-and acoinductivefun = 
+and acoinductivefun =
  id * identifier * aconstr * aconstr
 and explicit_named_substitution = id option * (uri * aconstr) list
 
@@ -101,7 +101,7 @@ type aobj =
  | AInductiveDefinition of id *
     anninductiveType list *                        (* inductive types ,      *)
     params * int                                   (*  parameters,n ind. pars*)
-and anninductiveType = 
+and anninductiveType =
  id * identifier * bool * aconstr *           (* typename, inductive, arity *)
   annconstructor list                         (*  constructors              *)
 and annconstructor =
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 64dc8a050..fb40ed86e 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -44,7 +44,7 @@ let print_term ids_to_inner_sorts =
          X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort]
      | A.AEvar (id,n,l) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "META" 
+         X.xml_nempty "META"
 	   ["no",(export_existential n) ; "id",id ; "sort",sort]
           (List.fold_left
             (fun i t ->
diff --git a/plugins/xml/cic2Xml.ml b/plugins/xml/cic2Xml.ml
index 08d3a8501..981503a66 100644
--- a/plugins/xml/cic2Xml.ml
+++ b/plugins/xml/cic2Xml.ml
@@ -6,7 +6,7 @@ let print_xml_term ch env sigma cic =
   let ids_to_inner_types = Hashtbl.create 503 in
   let seed = ref 0 in
   let acic =
-   Cic2acic.acic_of_cic_context' true seed ids_to_terms constr_to_ids 
+   Cic2acic.acic_of_cic_context' true seed ids_to_terms constr_to_ids
     ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
     env [] sigma (Unshare.unshare cic) None in
   let xml = Acic2Xml.print_term ids_to_inner_sorts acic in
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 1ac022159..5bb7635b9 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -22,12 +22,12 @@ let get_module_path_of_full_path path =
    List.filter
     (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
   with
-     [] -> 
+     [] ->
        Pp.warning ("Modules not supported: reference to "^
          Libnames.string_of_path path^" will be wrong");
        dirpath
    | [modul] -> modul
-   | _ -> 
+   | _ ->
        raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther
 ;;
 
@@ -134,7 +134,7 @@ let token_list_of_kernel_name ~keep_sections kn tag =
        else
         let module_path =
           let f = N.string_of_id (N.id_of_msid self) in
-          let _,longf = 
+          let _,longf =
             System.find_file_in_path (Library.get_load_path ()) (f^".v") in
           let ldir0 = Library.find_logical_path (Filename.dirname longf) in
           let id = Names.id_of_string (Filename.basename f) in
@@ -159,9 +159,9 @@ let token_list_of_kernel_name tag =
  let module N = Names in
  let module LN = Libnames in
  let id,dir = match tag with
-   | Variable kn -> 
+   | Variable kn ->
        N.id_of_label (N.label kn), Lib.cwd ()
-   | Constant con -> 
+   | Constant con ->
        N.id_of_label (N.con_label con),
        Lib.remove_section_part (LN.ConstRef con)
    | Inductive kn ->
@@ -211,7 +211,7 @@ module CPropRetyping =
         | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
         | _ -> Util.anomaly "Non-functional construction"
 
-                                                                                
+
   let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env ar =
     match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma ar) with
@@ -219,7 +219,7 @@ module CPropRetyping =
       | T.Sort s -> Coq_sort (T.family_of_sort s)
       | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
   in concl_of_arity env ft
-                                                                                
+
 let typeur sigma metamap =
   let rec type_of env cstr=
     match Term.kind_of_term cstr with
@@ -265,7 +265,7 @@ let typeur sigma metamap =
         | Coq_sort T.InSet -> T.mkSet
         | Coq_sort T.InType -> T.mkType Univ.type1_univ (* ERROR HERE *)
         | CProp -> T.mkConst DoubleTypeInference.cprop
-                                                                                
+
   and sort_of env t =
     match Term.kind_of_term t with
     | T.Cast (c,_, s) when T.isSort s -> family_of_term s
@@ -287,7 +287,7 @@ let typeur sigma metamap =
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
         Util.anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
-                                                                                
+
   and sort_family_of env t =
     match T.kind_of_term t with
     | T.Cast (c,_, s) when T.isSort s -> family_of_term s
@@ -299,7 +299,7 @@ let typeur sigma metamap =
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
         Util.anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
-                                                                                
+
   in type_of, sort_of, sort_family_of
 
   let get_type_of env sigma c = let f,_,_ = typeur sigma [] in f env c
@@ -484,7 +484,7 @@ print_endline "PASSATO" ; flush stdout ;
            (* an explicit named substitution of "type" *)
            (* (variable * argument) list, whose        *)
            (* second element is the list of residual   *)
-           (* arguments and whose third argument is    *) 
+           (* arguments and whose third argument is    *)
            (* the list of uninstantiated variables     *)
            let rec get_explicit_subst variables arguments =
             match variables,arguments with
@@ -497,7 +497,7 @@ print_endline "PASSATO" ; flush stdout ;
                 let he1'' =
                  String.concat "/"
                   (List.map Names.string_of_id (List.rev he1')) ^ "/"
-                 ^ (Names.string_of_id he1_id) ^ ".var" 
+                 ^ (Names.string_of_id he1_id) ^ ".var"
                 in
                  (he1'',he2)::subst, extra_args, uninst
            in
@@ -528,7 +528,7 @@ print_endline "PASSATO" ; flush stdout ;
          in
 
           (* Now that we have all the auxiliary functions we  *)
-          (* can finally proceed with the main case analysis. *) 
+          (* can finally proceed with the main case analysis. *)
           match T.kind_of_term tt with
              T.Rel n ->
               let id =
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 17d1d5dab..f8921aec9 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -69,12 +69,12 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
        T.Meta n ->
         Util.error
          "DoubleTypeInference.double_type_of: found a non-instanciated goal"
- 
+
      | T.Evar ((n,l) as ev) ->
         let ty = Unshare.unshare (Evd.existential_type sigma ev) in
         let jty = execute env sigma ty None in
         let jty = assumption_of_judgment env sigma jty in
-        let evar_context = 
+        let evar_context =
 	  E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in
          let rec iter actual_args evar_context =
           match actual_args,evar_context with
@@ -96,25 +96,25 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
           (* for side effects only *)
           iter (List.rev (Array.to_list l)) (List.rev evar_context) ;
           E.make_judge cstr jty
-	
-     | T.Rel n -> 
+
+     | T.Rel n ->
         Typeops.judge_of_relative env n
 
-     | T.Var id -> 
+     | T.Var id ->
         Typeops.judge_of_variable env id
-	  
+
      | T.Const c ->
         E.make_judge cstr (Typeops.type_of_constant env c)
-	  
+
      | T.Ind ind ->
         E.make_judge cstr (Inductiveops.type_of_inductive env ind)
-	  
-     | T.Construct cstruct -> 
+
+     | T.Construct cstruct ->
         E.make_judge cstr (Inductiveops.type_of_constructor env cstruct)
-	  
+
      | T.Case (ci,p,c,lf) ->
         let expectedtype =
-         Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in 
+         Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in
         let cj = execute env sigma c (Some expectedtype) in
         let pj = execute env sigma p None in
         let (expectedtypes,_,_) =
@@ -126,18 +126,18 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
           (Array.map (function x -> Some x) expectedtypes) in
         let (j,_) = Typeops.judge_of_case env ci pj cj lfj in
          j
-  
+
      | T.Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env sigma recdef in
         let fix = (vni,recdef') in
         E.make_judge (T.mkFix fix) tys.(i)
-	  
+
      | T.CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env sigma recdef in
         let cofix = (i,recdef') in
         E.make_judge (T.mkCoFix cofix) tys.(i)
-	  
-     | T.Sort (T.Prop c) -> 
+
+     | T.Sort (T.Prop c) ->
         Typeops.judge_of_prop_contents c
 
      | T.Sort (T.Type u) ->
@@ -153,8 +153,8 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 )
 
      | T.App (f,args) ->
-        let expected_head = 
-         Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma f) in 
+        let expected_head =
+         Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma f) in
         let j = execute env sigma f (Some expected_head) in
         let expected_args =
          let rec aux typ =
@@ -172,8 +172,8 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         let jl = execute_array env sigma args expected_args in
         let (j,_) = Typeops.judge_of_apply env j jl in
          j
-	    
-     | T.Lambda (name,c1,c2) -> 
+
+     | T.Lambda (name,c1,c2) ->
         let j = execute env sigma c1 None in
         let var = type_judgment env sigma j in
         let env1 = E.push_rel (name,None,var.E.utj_val) env in
@@ -186,9 +186,9 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
                   Some (Reductionops.nf_beta sigma expected_target_type)
                | _ -> assert false
         in
-        let j' = execute env1 sigma c2 expectedc2type in 
+        let j' = execute env1 sigma c2 expectedc2type in
          Typeops.judge_of_abstraction env1 name var j'
-	  
+
      | T.Prod (name,c1,c2) ->
         let j = execute env sigma c1 None in
         let varj = type_judgment env sigma j in
@@ -212,7 +212,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         in
          let j3 = execute env1 sigma c3 None in
           Typeops.judge_of_letin env name j1 j2 j3
-  
+
      | T.Cast (c,k,t) ->
         let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
         let tj = execute env sigma t None in
diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli
index 2e14b5580..b604ec4c4 100644
--- a/plugins/xml/doubleTypeInference.mli
+++ b/plugins/xml/doubleTypeInference.mli
@@ -12,7 +12,7 @@
 (*                       http://helm.cs.unibo.it                        *)
 (************************************************************************)
 
-type types = { synthesized : Term.types; expected : Term.types option; } 
+type types = { synthesized : Term.types; expected : Term.types option; }
 
 val cprop : Names.constant
 
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 407f86b36..82e90876d 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -42,7 +42,7 @@ let thin_sign osign sign =
 ;;
 
 let pr_tactic_xml = function
-  | TacArg (Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>" 
+  | TacArg (Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>"
   | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>"
 ;;
 
@@ -68,10 +68,10 @@ let pr_rule_xml pr = function
 let pr_var_decl_xml env (id,c,typ) =
   let ptyp = print_constr_env env typ in
   match c with
-  | None -> 
+  | None ->
       (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\"/>")
   | Some c ->
-      (* Force evaluation *) 
+      (* Force evaluation *)
       let pb = print_constr_env env c in
       (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\" body=\"" ++
          xmlstream pb ++ str "\"/>")
@@ -81,7 +81,7 @@ let pr_rel_decl_xml env (na,c,typ) =
   let pbody = match c with
     | None -> mt ()
     | Some c ->
-	(* Force evaluation *) 
+	(* Force evaluation *)
 	let pb = print_constr_env env c in
 	  (str" body=\"" ++ xmlstream pb ++ str "\"") in
   let ptyp = print_constr_env env typ in
@@ -108,8 +108,8 @@ let pr_context_xml env =
 ;;
 
 let pr_subgoal_metas_xml metas env=
-  let pr_one (meta, typ) = 
-    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++ 
+  let pr_one (meta, typ) =
+    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++
       str "\"/>"
   in
   List.fold_left (++) (mt ()) (List.map pr_one metas)
@@ -124,7 +124,7 @@ let pr_goal_xml g =
     (pr_context_xml env)) ++
     fnl () ++ str "</goal>")
   else
-    (hov 2 (str "<goal type=\"declarative\">" ++ 
+    (hov 2 (str "<goal type=\"declarative\">" ++
     (pr_context_xml env)) ++
     fnl () ++ str "</goal>")
 ;;
@@ -140,13 +140,13 @@ let rec print_proof_xml sigma osign pf =
         (List.fold_left (fun x y -> x ++ fnl () ++ y) (mt ()) (List.map (print_proof_xml sigma hyps) spfl))) ++ fnl () ++ str "</tree>"
 ;;
 
-let print_proof_xml () = 
-  let pp = print_proof_xml Evd.empty Sign.empty_named_context 
+let print_proof_xml () =
+  let pp = print_proof_xml Evd.empty Sign.empty_named_context
       (Tacmach.proof_of_pftreestate (Refiner.top_of_tree (Pfedit.get_pftreestate ())))
   in
   msgnl pp
 ;;
 
 VERNAC COMMAND EXTEND DumpTree
-  [ "Dump" "Tree" ] -> [ print_proof_xml () ] 
-END 
+  [ "Dump" "Tree" ] -> [ print_proof_xml () ]
+END
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml
index f7524671f..1beabf26c 100644
--- a/plugins/xml/proof2aproof.ml
+++ b/plugins/xml/proof2aproof.ml
@@ -63,8 +63,8 @@ let nf_evar sigma ~preserve =
 (* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
 let rec unshare_proof_tree =
  let module PT = Proof_type in
-  function {PT.open_subgoals = status ; 
-	    PT.goal = goal ; 
+  function {PT.open_subgoals = status ;
+	    PT.goal = goal ;
 	    PT.ref = ref} ->
    let unshared_ref =
     match ref with
@@ -78,8 +78,8 @@ let rec unshare_proof_tree =
 	in
          Some (unshared_rule, List.map unshare_proof_tree pfs)
    in
-    {PT.open_subgoals = status ; 
-     PT.goal = goal ; 
+    {PT.open_subgoals = status ;
+     PT.goal = goal ;
      PT.ref = unshared_ref}
 ;;
 
@@ -105,13 +105,13 @@ let extract_open_proof sigma pf =
     match node with
        {PT.ref=Some(PT.Prim _,_)} as pf ->
         L.prim_extractor proof_extractor vl pf
-	  
+
      | {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} ->
 	 let sgl,v = Refiner.frontier hidden_proof in
 	 let flat_proof = v spfl in
          ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ;
 	 proof_extractor vl flat_proof
-	  
+
      | {PT.ref=None;PT.goal=goal} ->
 	 let visible_rels =
            Util.map_succeed
@@ -124,14 +124,14 @@ let extract_open_proof sigma pf =
 (*CSC: it becomes a Rel; otherwise a Var. Then it can be already used  *)
 (*CSC: as the evar_instance. Ordering the instance becomes useless (it *)
 (*CSC: will already be ordered.                                        *)
-             (Termops.ids_of_named_context 
+             (Termops.ids_of_named_context
 		(Environ.named_context_of_val goal.Evd.evar_hyps)) in
 	 let sorted_rels =
 	   Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in
 	 let context =
-	   let l = 
+	   let l =
              List.map
-               (fun (_,id) -> Sign.lookup_named id 
+               (fun (_,id) -> Sign.lookup_named id
 		   (Environ.named_context_of_val goal.Evd.evar_hyps))
                sorted_rels in
 	   Environ.val_of_named_context l
@@ -144,7 +144,7 @@ let extract_open_proof sigma pf =
              evar_instance in
          evd := evd' ;
          evar
-	  
+
      | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor"
    in
     let unsharedconstr =
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 7503d6328..3f1e0a630 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -45,7 +45,7 @@ let constr_to_xml obj sigma env =
   let rel_context = Sign.push_named_to_rel_context named_context' [] in
   let rel_env =
    Environ.push_rel_context rel_context
-    (Environ.reset_with_named_context 
+    (Environ.reset_with_named_context
 	(Environ.val_of_named_context real_named_context) env) in
   let obj' =
    Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in
@@ -149,7 +149,7 @@ Pp.ppnl (Pp.(++) (Pp.str
          Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
         in begin
         match tactic_expr with
-        | T.TacArg (T.Tacexp _) -> 
+        | T.TacArg (T.Tacexp _) ->
             (* We don't need to keep the level of abstraction introduced at *)
             (* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
             aux flat_proof old_hyps
@@ -189,7 +189,7 @@ Pp.ppnl (Pp.(++) (Pp.str
         end
 
      | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} ->
-         Util.anomaly "Not Implemented" 
+         Util.anomaly "Not Implemented"
 
      | {PT.ref=Some(PT.Daimon,_)} ->
          X.xml_empty "Hidden_open_goal" of_attribute
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 4a27c3247..a46500b89 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -38,7 +38,7 @@ let print_if_verbose s = if !verbose then print_string s;;
 (* Next exception is used only inside print_coq_object and tag_of_string_tag *)
 exception Uninteresting;;
 
-(* NOT USED anymore, we back to the V6 point of view with global parameters 
+(* NOT USED anymore, we back to the V6 point of view with global parameters
 
 (* Internally, for Coq V7, params of inductive types are associated     *)
 (* not to the whole block of mutual inductive (as it was in V6) but to  *)
@@ -106,7 +106,7 @@ let filter_params pvars hyps =
    aux (Names.repr_dirpath modulepath) (List.rev pvars)
 ;;
 
-type variables_type = 
+type variables_type =
    Definition of string * Term.constr * Term.types
  | Assumption of string * Term.constr
 ;;
@@ -246,7 +246,7 @@ let find_hyps t =
    match T.kind_of_term t with
       T.Var id when not (List.mem id l) ->
        let (_,bo,ty) = Global.lookup_named id in
-        let boids = 
+        let boids =
          match bo with
             Some bo' -> aux l bo'
           | None -> l
@@ -393,7 +393,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
 (* The current channel for .theory files *)
 let theory_buffer = Buffer.create 4000;;
 
-let theory_output_string ?(do_not_quote = false) s = 
+let theory_output_string ?(do_not_quote = false) s =
   (* prepare for coqdoc post-processing *)
   let s = if do_not_quote then s else "(** #"^s^"\n#*)\n" in
   print_if_verbose s;
@@ -423,7 +423,7 @@ let kind_of_variable id =
     | _ -> Util.anomaly "Unsupported variable kind"
 ;;
 
-let kind_of_constant kn = 
+let kind_of_constant kn =
   let module DK = Decl_kinds in
   match Decls.constant_kind kn with
     | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
@@ -432,7 +432,7 @@ let kind_of_constant kn =
         Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
         "AXIOM","Declaration"
     | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
-    | DK.IsDefinition DK.Example -> 
+    | DK.IsDefinition DK.Example ->
         Pp.warning "Example not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.Coercion ->
@@ -461,10 +461,10 @@ let kind_of_constant kn =
         "DEFINITION","Definition"
     | DK.IsDefinition DK.Instance ->
         Pp.warning "Instance not supported in dtd (used Definition instead)";
-        "DEFINITION","Definition" 
+        "DEFINITION","Definition"
     | DK.IsDefinition DK.Method ->
         Pp.warning "Method not supported in dtd (used Definition instead)";
-        "DEFINITION","Definition" 
+        "DEFINITION","Definition"
     | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
         "THEOREM",DK.string_of_theorem_kind thm
     | DK.IsProof _ ->
@@ -476,7 +476,7 @@ let kind_of_global r =
   let module Ln = Libnames in
   let module DK = Decl_kinds in
   match r with
-  | Ln.IndRef kn | Ln.ConstructRef (kn,_) -> 
+  | Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
       let isrecord =
 	try let _ = Recordops.lookup_projections kn in true
         with Not_found -> false in
@@ -515,7 +515,7 @@ let print internal glob_ref kind xml_library_root =
    match glob_ref with
       Ln.VarRef id ->
        (* this kn is fake since it is not provided by Coq *)
-       let kn = 
+       let kn =
         let (mod_path,dir_path) = Lib.current_prefix () in
         N.make_kn mod_path dir_path (N.label_of_id id)
        in
@@ -615,13 +615,13 @@ let _ =
    (function (internal,kn) ->
      match !proof_to_export with
         None ->
-          print internal (Libnames.ConstRef kn) (kind_of_constant kn) 
+          print internal (Libnames.ConstRef kn) (kind_of_constant kn)
 	    xml_library_root
       | Some pftreestate ->
          (* It is a proof. Let's export it starting from the proof-tree *)
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
         let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
-         show_pftreestate internal fn pftreestate 
+         show_pftreestate internal fn pftreestate
 	  (Names.id_of_label (Names.con_label kn)) ;
          proof_to_export := None)
 ;;
@@ -629,7 +629,7 @@ let _ =
 let _ =
   Declare.set_xml_declare_inductive
    (function (isrecord,(sp,kn)) ->
-      print false (Libnames.IndRef (kn,0)) (kind_of_inductive isrecord kn) 
+      print false (Libnames.IndRef (kn,0)) (kind_of_inductive isrecord kn)
         xml_library_root)
 ;;
 
@@ -664,7 +664,7 @@ let _ =
              Buffer.output_buffer ch theory_buffer ;
              close_out ch
        end ;
-       Option.iter 
+       Option.iter
 	(fun fn ->
 	  let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
@@ -684,7 +684,7 @@ let _ =
 let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;;
 
 let uri_of_dirpath dir =
-  "/" ^ String.concat "/" 
+  "/" ^ String.concat "/"
     (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir)))
 ;;
 
@@ -702,7 +702,7 @@ let _ =
 
 let _ =
   Library.set_xml_require
-    (fun d -> theory_output_string 
+    (fun d -> theory_output_string
       (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
        (uri_of_dirpath d) (Names.string_of_dirpath d)))
 ;;