diff options
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 41 |
1 files changed, 19 insertions, 22 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 01271323..3c4b01f5 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -73,11 +73,7 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *) let tag = Libobject.object_tag o in print_if_verbose ("Object tag: " ^ tag ^ "\n") ; match tag with - "CONSTANT" -> - (match D.constant_strength sp with - | DK.Local -> false (* a local definition *) - | DK.Global -> true (* a non-local one *) - ) + "CONSTANT" -> true (* constants/parameters are non global *) | "INDUCTIVE" -> true (* mutual inductive types are never local *) | "VARIABLE" -> false (* variables are local, so no namesakes *) | _ -> false (* uninteresting thing that won't be printed*) @@ -89,8 +85,7 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *) (* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT *) (* SECTION, WHOSE PATH IS namei *) -let pvars = - ref ([Names.id_of_string "",[]] : (Names.identifier * string list) list);; +let pvars = ref ([] : string list);; let cumenv = ref Environ.empty_env;; (* filter_params pvars hyps *) @@ -138,9 +133,7 @@ let add_to_pvars x = E.push_named (Names.id_of_string v, None, typ) !cumenv ; v in - match !pvars with - [] -> assert false - | ((name,l)::tl) -> pvars := (name,v::l)::tl + pvars := v::!pvars ;; (* The computation is very inefficient, but we can't do anything *) @@ -157,7 +150,7 @@ let search_variables () = | he::tl as modules -> let one_section_variables = let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in - let t = List.map N.string_of_id (Declare.last_section_hyps dirpath) in + let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in [he,t] in one_section_variables @ aux tl @@ -329,14 +322,13 @@ let mk_variable_obj id body typ = let variables = search_variables () in let params = filter_params variables hyps'' in Acic.Variable - (Names.string_of_id id, unsharedbody, - (Unshare.unshare (Term.body_of_type typ)), params) + (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params) ;; (* Unsharing is not performed on the body, that must be already unshared. *) (* The evar map and the type, instead, are unshared by this function. *) let mk_current_proof_obj is_a_variable id bo ty evar_map env = - let unshared_ty = Unshare.unshare (Term.body_of_type ty) in + let unshared_ty = Unshare.unshare ty in let metasenv = List.map (function @@ -384,7 +376,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env = let mk_constant_obj id bo ty variables hyps = let hyps = string_list_of_named_context_list hyps in - let ty = Unshare.unshare (Term.body_of_type ty) in + let ty = Unshare.unshare ty in let params = filter_params variables hyps in match bo with None -> @@ -413,7 +405,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) (Array.mapi - (fun j x ->(x,Unshare.unshare (Term.body_of_type lc.(j)))) consnames) + (fun j x ->(x,Unshare.unshare lc.(j))) consnames) [] ) in @@ -447,7 +439,7 @@ let kind_of_inductive isrecord kn = let kind_of_variable id = let module DK = Decl_kinds in - match Declare.variable_kind id with + match Decls.variable_kind id with | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption" | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis" | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture" @@ -458,7 +450,7 @@ let kind_of_variable id = let kind_of_constant kn = let module DK = Decl_kinds in - match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with + match Decls.constant_kind kn with | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" | DK.IsAssumption DK.Conjectural -> @@ -492,6 +484,12 @@ let kind_of_constant kn = | DK.IsDefinition DK.IdentityCoercion -> Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" + | DK.IsDefinition DK.Instance -> + Pp.warning "Instance not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Method -> + Pp.warning "Method not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> @@ -541,11 +539,10 @@ let print internal glob_ref kind xml_library_root = let tag,obj = match glob_ref with Ln.VarRef id -> - let sp = Declare.find_section_variable id in (* this kn is fake since it is not provided by Coq *) let kn = let (mod_path,dir_path) = Lib.current_prefix () in - N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp)) + N.make_kn mod_path dir_path (N.label_of_id id) in let (_,body,typ) = G.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ @@ -692,11 +689,11 @@ let _ = Buffer.output_buffer ch theory_buffer ; close_out ch end ; - Util.option_iter + Option.iter (fun fn -> let coqdoc = Coq_config.bindir^"/coqdoc" in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in - let dir = Util.out_some xml_library_root in + let dir = Option.get xml_library_root in let command cmd = if Sys.command cmd <> 0 then Util.anomaly ("Error executing \"" ^ cmd ^ "\"") |