summaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/cic2Xml.ml2
-rw-r--r--contrib/xml/cic2acic.ml10
-rw-r--r--contrib/xml/proofTree2Xml.ml44
-rw-r--r--contrib/xml/xmlcommand.ml29
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:42:54 +0000