Fixing #1960 (xml bug with external on goal variable) and #1961

(anomaly while parsing $ not followed by an ident).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11785 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 26 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 4ee97813bd..1ae1866144 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -79,15 +79,6 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
     | _                 -> false  (* uninteresting thing that won't be printed*)
 ;;
 
-
-(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *)
-(* ENVIRONMENT (= [(name1,l1); ...;(namen,ln)] WHERE li IS THE LIST *)
-(* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT   *)
-(* SECTION, WHOSE PATH IS namei                                     *)
-
-let pvars = ref ([] : string list);;
-let cumenv = ref Environ.empty_env;;
-
 (* filter_params pvars hyps *)
 (* filters out from pvars (which is a list of lists) all the variables *)
 (* that does not belong to hyps (which is a simple list)               *)
@@ -120,22 +111,6 @@ type variables_type =
  | Assumption of string * Term.constr
 ;;
 
-let add_to_pvars x =
- let module E = Environ in
-  let v =
-   match x with
-      Definition (v, bod, typ) ->
-       cumenv :=
-         E.push_named (Names.id_of_string v, Some bod, typ) !cumenv ;
-       v
-    | Assumption (v, typ) ->
-       cumenv :=
-         E.push_named (Names.id_of_string v, None, typ) !cumenv ;
-       v
-  in
-  pvars := v::!pvars
-;;
-
 (* The computation is very inefficient, but we can't do anything *)
 (* better unless this function is reimplemented in the Declare   *)
 (* module.                                                       *)
@@ -231,7 +206,7 @@ let print_object uri obj sigma proof_tree_infos filename =
        ignore (Unix.system ("gzip " ^ fn' ^ ".xml"))
  in
   let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) =
-   Cic2acic.acic_object_of_cic_object !pvars sigma obj in
+   Cic2acic.acic_object_of_cic_object sigma obj in
   let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in
   let xmltypes =
    Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in