Imported Upstream version 8.4~betaupstream/8.4_beta

15 files changed, 42 insertions, 195 deletions

diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml
index 97287d18..653c2b7b 100644
--- a/plugins/xml/acic.ml
+++ b/plugins/xml/acic.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 631af9f0..97f7e2bd 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 0b98acd2..da0a65ff 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index d67c114e..a21a919a 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
@@ -27,7 +27,7 @@ let cprop =
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
- let module R = Rawterm in
+ let module R = Glob_term in
  let module C = Closure in
  let module CR = C.RedFlags in
  (*** CProp is made Opaque ***)
diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli
index 3858b906..5c00bdc6 100644
--- a/plugins/xml/doubleTypeInference.mli
+++ b/plugins/xml/doubleTypeInference.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 3cfc52b7..3c3e54fa 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 "\"/>"
 ;;
 
@@ -56,13 +56,11 @@ let pr_rule_xml pr = function
       hov 2 (str "<cmpdrule>" ++ fnl () ++
         begin match cmpd with
           Tactic (texp, _) -> pr_tactic_xml texp
-        | Proof_instr (_,instr) -> pr_proof_instr_xml instr
         end ++ fnl ()
         ++ pr subtree
       ) ++ fnl () ++ str "</cmpdrule>"
   | Daimon -> str "<daimon/>"
   | Decl_proof _ -> str "<proof/>"
-(*  | Change_evars -> str "<chgevars/>"*)
 ;;
 
 let pr_var_decl_xml env (id,c,typ) =
@@ -115,11 +113,11 @@ let pr_subgoal_metas_xml metas env=
   List.fold_left (++) (mt ()) (List.map pr_one metas)
 ;;
 
-let pr_goal_xml g =
-  let env = try evar_unfiltered_env g with _ -> empty_env in
-  if g.evar_extra = None then
+let pr_goal_xml sigma g =
+  let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in
+  if Decl_mode.try_get_info sigma g = None then
     (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
-    xmlstream (pr_ltype_env_at_top env g.evar_concl) ++
+    xmlstream (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) ++
     str "\"/>" ++
     (pr_context_xml env)) ++
     fnl () ++ str "</goal>")
@@ -129,23 +127,9 @@ let pr_goal_xml g =
     fnl () ++ str "</goal>")
 ;;
 
-let rec print_proof_xml sigma osign pf =
-  let hyps = Environ.named_context_of_val pf.goal.evar_hyps in
-  let hyps' = thin_sign osign hyps in
-  match pf.ref with
-    | None -> hov 2 (str "<tree>" ++ fnl () ++ (pr_goal_xml {pf.goal with evar_hyps=hyps'})) ++ fnl () ++ str "</tree>"
-    | Some(r,spfl) ->
-        hov 2 (str "<tree>" ++ fnl () ++
-        (pr_goal_xml {pf.goal with evar_hyps=hyps'}) ++ fnl () ++ (pr_rule_xml (print_proof_xml sigma osign) r) ++
-        (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
-      (Tacmach.proof_of_pftreestate (Refiner.top_of_tree (Pfedit.get_pftreestate ())))
-  in
-  msgnl pp
-;;
+  Util.anomaly "Dump Tree command not supported in this version."
+
 
 VERNAC COMMAND EXTEND DumpTree
   [ "Dump" "Tree" ] -> [ print_proof_xml () ]
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml
index d871935b..2d16190b 100644
--- a/plugins/xml/proof2aproof.ml
+++ b/plugins/xml/proof2aproof.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
@@ -59,30 +59,6 @@ let nf_evar sigma ~preserve =
     aux
 ;;
 
-(* Unshares a proof-tree.                                                  *)
-(* 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 ;
-	    PT.ref = ref} ->
-   let unshared_ref =
-    match ref with
-       None -> None
-     | Some (rule,pfs) ->
-        let unshared_rule =
-         match rule with
-             PT.Nested (cmpd, pf) ->
-               PT.Nested (cmpd, unshare_proof_tree pf)
-	   | other -> other
-	in
-         Some (unshared_rule, List.map unshare_proof_tree pfs)
-   in
-    {PT.open_subgoals = status ;
-     PT.goal = goal ;
-     PT.ref = unshared_ref}
-;;
-
 module ProofTreeHash =
  Hashtbl.Make
   (struct
@@ -94,83 +70,9 @@ module ProofTreeHash =
 
 
 let extract_open_proof sigma pf =
- let module PT = Proof_type in
- let module L = Logic in
-  let evd = ref (Evd.create_evar_defs sigma) in
-  let proof_tree_to_constr = ProofTreeHash.create 503 in
-  let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in
-  let unshared_constrs = ref S.empty in
-  let rec proof_extractor vl node =
-   let constr =
-    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
-             (fun id ->
-                (* Section variables are in the [id] list but are not *)
-                (* lambda abstracted in the term [vl]                 *)
-                try let n = Logic.proof_variable_index id vl in (n,id)
-	        with Not_found -> failwith "caught")
-(*CSC: the above function must be modified such that when it is found  *)
-(*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
-		(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 =
-             List.map
-               (fun (_,id) -> Sign.lookup_named id
-		   (Environ.named_context_of_val goal.Evd.evar_hyps))
-               sorted_rels in
-	   Environ.val_of_named_context l
-         in
-(*CSC: the section variables in the right order must be added too *)
-         let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in
-    (*     let env = Global.env_of_context context in *)
-	 let evd',evar =
-           Evarutil.new_evar_instance context !evd goal.Evd.evar_concl
-             evar_instance in
-         evd := evd' ;
-         evar
-
-     | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor"
-   in
-    let unsharedconstr =
-     let evar_nf_constr =
-      nf_evar ( !evd)
-        ~preserve:(function e -> S.mem e !unshared_constrs) constr
-     in
-      Unshare.unshare
-       ~already_unshared:(function e -> S.mem e !unshared_constrs)
-       evar_nf_constr
-    in
-(*CSC: debugging stuff to be removed *)
-if ProofTreeHash.mem proof_tree_to_constr node then
- Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ")
- (Tactic_printer.print_proof ( !evd) [] node)) ;
-     ProofTreeHash.add proof_tree_to_constr node unsharedconstr ;
-     unshared_constrs := S.add unsharedconstr !unshared_constrs ;
-     unsharedconstr
-  in
-  let unshared_pf = unshare_proof_tree pf in
-  let pfterm = proof_extractor [] unshared_pf in
-   (pfterm,  !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
-    unshared_pf)
-;;
+  (* Deactivated and candidate for removal. (Apr. 2010) *)
+   ()
 
 let extract_open_pftreestate pts =
-  extract_open_proof (Refiner.evc_of_pftreestate pts)
-   (Tacmach.proof_of_pftreestate pts)
-;;
+  (* Deactivated and candidate for removal. (Apr. 2010) *)
+   ()
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 21c86c79..2f5eb6ac 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
@@ -14,11 +14,6 @@
 
 let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";;
 
-let std_ppcmds_to_string s =
-   Pp.msg_with Format.str_formatter s;
-   Format.flush_str_formatter ()
-;;
-
 let idref_of_id id = "v" ^ id;;
 
 (* Transform a constr to an Xml.token Stream.t *)
@@ -149,22 +144,24 @@ 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
         | _ ->
          (****** la tactique employee *)
 	 let prtac = Pptactic.pr_tactic (Global.env()) in
-         let tac = std_ppcmds_to_string (prtac tactic_expr) in
+         let tac = Pp.string_of_ppcmds (prtac tactic_expr) in
          let tacname= first_word tac in
          let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
 
          (****** le but *)
-         let {Evd.evar_concl=concl;
-              Evd.evar_hyps=hyps}=goal in
+
+	 let concl = Goal.V82.concl sigma goal in
+	 let hyps = Goal.V82.hyps sigma goal in
 
          let env = Global.env_of_context hyps in
+	   
 
          let xgoal =
           X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
@@ -188,14 +185,12 @@ Pp.ppnl (Pp.(++) (Pp.str
           [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
         end
 
-     | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} ->
-         Util.anomaly "Not Implemented"
-
      | {PT.ref=Some(PT.Daimon,_)} ->
          X.xml_empty "Hidden_open_goal" of_attribute
 
      | {PT.ref=None;PT.goal=goal} ->
          X.xml_empty "Open_goal" of_attribute
+     | {PT.ref=Some(PT.Decl_proof _, _)} -> failwith "TODO: xml and decl_proof"
   in
    [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
       X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n");
diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml
index 344a1581..c854427d 100644
--- a/plugins/xml/unshare.ml
+++ b/plugins/xml/unshare.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
diff --git a/plugins/xml/unshare.mli b/plugins/xml/unshare.mli
index 4b96b22e..cace2de6 100644
--- a/plugins/xml/unshare.mli
+++ b/plugins/xml/unshare.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4
index 2d73074b..8a4eb39a 100644
--- a/plugins/xml/xml.ml4
+++ b/plugins/xml/xml.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
diff --git a/plugins/xml/xml.mli b/plugins/xml/xml.mli
index ffaad957..0b6d5198 100644
--- a/plugins/xml/xml.mli
+++ b/plugins/xml/xml.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
@@ -12,8 +12,6 @@
 (*                       http://helm.cs.unibo.it                        *)
 (************************************************************************)
 
-(*i $Id: xml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* Tokens for XML cdata, empty elements and not-empty elements           *)
 (* Usage:                                                                *)
 (*  Str cdata                                                            *)
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 7e7f890f..1037bbf0 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
@@ -527,8 +527,10 @@ let print internal glob_ref kind xml_library_root =
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Ln.ConstRef kn ->
        let id = N.id_of_label (N.con_label kn) in
-       let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
-        G.lookup_constant kn in
+       let cb = G.lookup_constant kn in
+       let val0 = D.body_of_constant cb in
+       let typ = cb.D.const_type in
+       let hyps = cb.D.const_hyps in
        let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
@@ -557,43 +559,13 @@ let print_ref qid fn =
 (*  where dest is either None (for stdout) or (Some filename) *)
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 let show_pftreestate internal fn (kind,pftst) id =
- let pf = Tacmach.proof_of_pftreestate pftst in
- let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in
- let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree,
-     unshared_pf
- =
-  Proof2aproof.extract_open_pftreestate pftst in
- let env = Global.env () in
- let obj =
-  mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in
- let uri =
-  match kind with
-     Decl_kinds.Local, _ ->
-      let uri =
-       "cic:/" ^ String.concat "/"
-        (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable)
-      in
-      let kind_of_var = "VARIABLE","LocalFact" in
-      (match internal with
-       | Declare.KernelSilent -> ()
-       | _ -> print_object_kind uri kind_of_var
-       ); uri
-   | Decl_kinds.Global, _ ->
-      let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in
-      (match internal with
-       | Declare.KernelSilent -> ()
-       | _ -> print_object_kind uri (kind_of_global_goal kind)
-      ); uri
- in
-  print_object uri obj evar_map
-   (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr,
-    proof_tree_to_flattened_proof_tree)) fn
-;;
+ if true then
+   Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version."
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
  let (id,kind,_,_) = Pfedit.current_proof_statement () in
-  show_pftreestate Declare.KernelVerbose fn (kind,pftst) id
+  show_pftreestate false fn (kind,pftst) id
 ;;
 
 
@@ -680,7 +652,7 @@ let _ =
        end ;
        Option.iter
 	(fun fn ->
-	  let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
+	  let coqdoc = Filename.concat Envars.coqbin ("coqdoc" ^ Coq_config.exec_extension) in
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
           let command cmd =
            if Sys.command cmd <> 0 then
diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli
index eadf3cfd..ec50d623 100644
--- a/plugins/xml/xmlcommand.mli
+++ b/plugins/xml/xmlcommand.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
@@ -12,8 +12,6 @@
 (*                       http://helm.cs.unibo.it                        *)
 (************************************************************************)
 
-(*i $Id: xmlcommand.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* print_global qid fn                                                    *)
 (*  where qid  is a long name denoting a definition/theorem or            *)
 (*             an inductive definition                                    *)
diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4
index f9d5bac0..d65a1bd3 100644
--- a/plugins/xml/xmlentries.ml4
+++ b/plugins/xml/xmlentries.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 (*         *   University of Bologna                                    *)
@@ -14,8 +14,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: xmlentries.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util;;
 open Vernacinterp;;