diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/xml/xmlcommand.ml | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
-rw-r--r-- | contrib/xml/xmlcommand.ml | 29 |
1 files changed, 2 insertions, 27 deletions
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 = |