Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

4 files changed, 12 insertions, 33 deletions

diff --git a/contrib/xml/cic2Xml.ml b/contrib/xml/cic2Xml.ml
index f04a03f9..08d3a850 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 1a6cb9c8..c62db00b 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 05be01bc..a501fb6a 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
@@ -91,6 +90,7 @@ let string_of_prim_rule x = match x with
   | Proof_type.Thin _ -> "Thin"
   | Proof_type.ThinBody _-> "ThinBody"
   | Proof_type.Move (_,_,_) -> "Move"
+  | Proof_type.Order _ -> "Order"
   | Proof_type.Rename (_,_) -> "Rename"
   | Proof_type.Change_evars -> "Change_evars"
 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3c4b01f5..1ae18661 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
@@ -691,7 +666,7 @@ let _ =
        end ;
        Option.iter 
 	(fun fn ->
-	  let coqdoc = Coq_config.bindir^"/coqdoc" 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 dir = Option.get xml_library_root in
           let command cmd =