diff options
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 = |