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

4 files changed, 10 insertions, 32 deletions

diff --git a/contrib/xml/cic2Xml.ml b/contrib/xml/cic2Xml.ml
index f04a03f9fd..08d3a85010 100644
--- a/contrib/xml/cic2Xml.ml
+++ b/contrib/xml/cic2Xml.ml
@@ -7,7 +7,7 @@ let print_xml_term ch env sigma cic =
   let seed = ref 0 in
   let acic =
    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 []
+    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
   Xml.pp_ch xml ch
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 1a6cb9c811..c62db00bb1 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -349,7 +349,7 @@ let source_id_of_id id = "#source#" ^ id;;
 
 let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
  ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
- pvars ?(fake_dependent_products=false) env idrefs evar_map t expectedty
+ ?(fake_dependent_products=false) env idrefs evar_map t expectedty
 =
  let module D = DoubleTypeInference in
  let module E = Environ in
@@ -541,6 +541,8 @@ print_endline "PASSATO" ; flush stdout ;
                 add_inner_type fresh_id'' ;
                A.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
            | T.Var id ->
+	      let pvars = Termops.ids_of_named_context (E.named_context env) in
+	      let pvars = List.map N.string_of_id pvars in
               let path = get_uri_of_var (N.string_of_id id) pvars in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
@@ -827,6 +829,7 @@ print_endline "PASSATO" ; flush stdout ;
      aux computeinnertypes None [] env idrefs t
 ;;
 
+(* Obsolete [HH 1/2009]
 let acic_of_cic_context metasenv context t =
  let ids_to_terms = Hashtbl.create 503 in
  let constr_to_ids = Acic.CicHash.create 503 in
@@ -838,8 +841,9 @@ let acic_of_cic_context metasenv context t =
     ids_to_inner_sorts ids_to_inner_types metasenv context t,
    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 ;;
+*)
 
-let acic_object_of_cic_object pvars sigma obj =
+let acic_object_of_cic_object sigma obj =
  let module A = Acic in
   let ids_to_terms = Hashtbl.create 503 in
   let constr_to_ids = Acic.CicHash.create 503 in
@@ -853,7 +857,7 @@ let acic_object_of_cic_object pvars sigma obj =
   let seed = ref 0 in
   let acic_term_of_cic_term_context' =
    acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids
-    ids_to_inner_sorts ids_to_inner_types pvars in
+    ids_to_inner_sorts ids_to_inner_types in
 (*CSC: is this the right env to use? Hhmmm. There is a problem: in    *)
 (*CSC: Global.env () the object we are exporting is already defined,  *)
 (*CSC: either in the environment or in the named context (in the case *)
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 26b1b0b760..a501fb6a63 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -31,7 +31,6 @@ let constr_to_xml obj sigma env =
   let ids_to_inner_sorts = Hashtbl.create 503 in
   let ids_to_inner_types = Hashtbl.create 503 in
 
-  let pvars = [] in
   (* named_context holds section variables and local variables *)
   let named_context = Environ.named_context env  in
   (* real_named_context holds only the section variables *)
@@ -54,7 +53,7 @@ let constr_to_xml obj sigma env =
    try
     let annobj =
      Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids
-      ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars rel_env
+      ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env
       idrefs sigma (Unshare.unshare obj') None
     in
      Acic2Xml.print_term ids_to_inner_sorts annobj
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