diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /plugins/xml | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'plugins/xml')
-rw-r--r-- | plugins/xml/acic.ml | 2 | ||||
-rw-r--r-- | plugins/xml/acic2Xml.ml4 | 2 | ||||
-rw-r--r-- | plugins/xml/cic2acic.ml | 2 | ||||
-rw-r--r-- | plugins/xml/doubleTypeInference.ml | 4 | ||||
-rw-r--r-- | plugins/xml/doubleTypeInference.mli | 2 | ||||
-rw-r--r-- | plugins/xml/dumptree.ml4 | 32 | ||||
-rw-r--r-- | plugins/xml/proof2aproof.ml | 108 | ||||
-rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 21 | ||||
-rw-r--r-- | plugins/xml/unshare.ml | 2 | ||||
-rw-r--r-- | plugins/xml/unshare.mli | 2 | ||||
-rw-r--r-- | plugins/xml/xml.ml4 | 2 | ||||
-rw-r--r-- | plugins/xml/xml.mli | 4 | ||||
-rw-r--r-- | plugins/xml/xmlcommand.ml | 46 | ||||
-rw-r--r-- | plugins/xml/xmlcommand.mli | 4 | ||||
-rw-r--r-- | plugins/xml/xmlentries.ml4 | 4 |
15 files changed, 42 insertions, 195 deletions
diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml index 97287d18..653c2b7b 100644 --- a/plugins/xml/acic.ml +++ b/plugins/xml/acic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 631af9f0..97f7e2bd 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 0b98acd2..da0a65ff 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index d67c114e..a21a919a 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -27,7 +27,7 @@ let cprop = ;; let whd_betadeltaiotacprop env _evar_map ty = - let module R = Rawterm in + let module R = Glob_term in let module C = Closure in let module CR = C.RedFlags in (*** CProp is made Opaque ***) diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli index 3858b906..5c00bdc6 100644 --- a/plugins/xml/doubleTypeInference.mli +++ b/plugins/xml/doubleTypeInference.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 3cfc52b7..3c3e54fa 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -42,7 +42,7 @@ let thin_sign osign sign = ;; let pr_tactic_xml = function - | TacArg (Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>" + | TacArg (_,Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>" | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>" ;; @@ -56,13 +56,11 @@ let pr_rule_xml pr = function hov 2 (str "<cmpdrule>" ++ fnl () ++ begin match cmpd with Tactic (texp, _) -> pr_tactic_xml texp - | Proof_instr (_,instr) -> pr_proof_instr_xml instr end ++ fnl () ++ pr subtree ) ++ fnl () ++ str "</cmpdrule>" | Daimon -> str "<daimon/>" | Decl_proof _ -> str "<proof/>" -(* | Change_evars -> str "<chgevars/>"*) ;; let pr_var_decl_xml env (id,c,typ) = @@ -115,11 +113,11 @@ let pr_subgoal_metas_xml metas env= List.fold_left (++) (mt ()) (List.map pr_one metas) ;; -let pr_goal_xml g = - let env = try evar_unfiltered_env g with _ -> empty_env in - if g.evar_extra = None then +let pr_goal_xml sigma g = + let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in + if Decl_mode.try_get_info sigma g = None then (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++ - xmlstream (pr_ltype_env_at_top env g.evar_concl) ++ + xmlstream (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) ++ str "\"/>" ++ (pr_context_xml env)) ++ fnl () ++ str "</goal>") @@ -129,23 +127,9 @@ let pr_goal_xml g = fnl () ++ str "</goal>") ;; -let rec print_proof_xml sigma osign pf = - let hyps = Environ.named_context_of_val pf.goal.evar_hyps in - let hyps' = thin_sign osign hyps in - match pf.ref with - | None -> hov 2 (str "<tree>" ++ fnl () ++ (pr_goal_xml {pf.goal with evar_hyps=hyps'})) ++ fnl () ++ str "</tree>" - | Some(r,spfl) -> - hov 2 (str "<tree>" ++ fnl () ++ - (pr_goal_xml {pf.goal with evar_hyps=hyps'}) ++ fnl () ++ (pr_rule_xml (print_proof_xml sigma osign) r) ++ - (List.fold_left (fun x y -> x ++ fnl () ++ y) (mt ()) (List.map (print_proof_xml sigma hyps) spfl))) ++ fnl () ++ str "</tree>" -;; - let print_proof_xml () = - let pp = print_proof_xml Evd.empty Sign.empty_named_context - (Tacmach.proof_of_pftreestate (Refiner.top_of_tree (Pfedit.get_pftreestate ()))) - in - msgnl pp -;; + Util.anomaly "Dump Tree command not supported in this version." + VERNAC COMMAND EXTEND DumpTree [ "Dump" "Tree" ] -> [ print_proof_xml () ] diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml index d871935b..2d16190b 100644 --- a/plugins/xml/proof2aproof.ml +++ b/plugins/xml/proof2aproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -59,30 +59,6 @@ let nf_evar sigma ~preserve = aux ;; -(* Unshares a proof-tree. *) -(* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *) -let rec unshare_proof_tree = - let module PT = Proof_type in - function {PT.open_subgoals = status ; - PT.goal = goal ; - PT.ref = ref} -> - let unshared_ref = - match ref with - None -> None - | Some (rule,pfs) -> - let unshared_rule = - match rule with - PT.Nested (cmpd, pf) -> - PT.Nested (cmpd, unshare_proof_tree pf) - | other -> other - in - Some (unshared_rule, List.map unshare_proof_tree pfs) - in - {PT.open_subgoals = status ; - PT.goal = goal ; - PT.ref = unshared_ref} -;; - module ProofTreeHash = Hashtbl.Make (struct @@ -94,83 +70,9 @@ module ProofTreeHash = let extract_open_proof sigma pf = - let module PT = Proof_type in - let module L = Logic in - let evd = ref (Evd.create_evar_defs sigma) in - let proof_tree_to_constr = ProofTreeHash.create 503 in - let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in - let unshared_constrs = ref S.empty in - let rec proof_extractor vl node = - let constr = - match node with - {PT.ref=Some(PT.Prim _,_)} as pf -> - L.prim_extractor proof_extractor vl pf - - | {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} -> - let sgl,v = Refiner.frontier hidden_proof in - let flat_proof = v spfl in - ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ; - proof_extractor vl flat_proof - - | {PT.ref=None;PT.goal=goal} -> - let visible_rels = - Util.map_succeed - (fun id -> - (* Section variables are in the [id] list but are not *) - (* lambda abstracted in the term [vl] *) - try let n = Logic.proof_variable_index id vl in (n,id) - with Not_found -> failwith "caught") -(*CSC: the above function must be modified such that when it is found *) -(*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *) -(*CSC: as the evar_instance. Ordering the instance becomes useless (it *) -(*CSC: will already be ordered. *) - (Termops.ids_of_named_context - (Environ.named_context_of_val goal.Evd.evar_hyps)) in - let sorted_rels = - Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in - let context = - let l = - List.map - (fun (_,id) -> Sign.lookup_named id - (Environ.named_context_of_val goal.Evd.evar_hyps)) - sorted_rels in - Environ.val_of_named_context l - in -(*CSC: the section variables in the right order must be added too *) - let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in - (* let env = Global.env_of_context context in *) - let evd',evar = - Evarutil.new_evar_instance context !evd goal.Evd.evar_concl - evar_instance in - evd := evd' ; - evar - - | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor" - in - let unsharedconstr = - let evar_nf_constr = - nf_evar ( !evd) - ~preserve:(function e -> S.mem e !unshared_constrs) constr - in - Unshare.unshare - ~already_unshared:(function e -> S.mem e !unshared_constrs) - evar_nf_constr - in -(*CSC: debugging stuff to be removed *) -if ProofTreeHash.mem proof_tree_to_constr node then - Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") - (Tactic_printer.print_proof ( !evd) [] node)) ; - ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; - unshared_constrs := S.add unsharedconstr !unshared_constrs ; - unsharedconstr - in - let unshared_pf = unshare_proof_tree pf in - let pfterm = proof_extractor [] unshared_pf in - (pfterm, !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, - unshared_pf) -;; + (* Deactivated and candidate for removal. (Apr. 2010) *) + () let extract_open_pftreestate pts = - extract_open_proof (Refiner.evc_of_pftreestate pts) - (Tacmach.proof_of_pftreestate pts) -;; + (* Deactivated and candidate for removal. (Apr. 2010) *) + () diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index 21c86c79..2f5eb6ac 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -14,11 +14,6 @@ let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";; -let std_ppcmds_to_string s = - Pp.msg_with Format.str_formatter s; - Format.flush_str_formatter () -;; - let idref_of_id id = "v" ^ id;; (* Transform a constr to an Xml.token Stream.t *) @@ -149,22 +144,24 @@ Pp.ppnl (Pp.(++) (Pp.str Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node in begin match tactic_expr with - | T.TacArg (T.Tacexp _) -> + | T.TacArg (_,T.Tacexp _) -> (* We don't need to keep the level of abstraction introduced at *) (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) aux flat_proof old_hyps | _ -> (****** la tactique employee *) let prtac = Pptactic.pr_tactic (Global.env()) in - let tac = std_ppcmds_to_string (prtac tactic_expr) in + let tac = Pp.string_of_ppcmds (prtac tactic_expr) in let tacname= first_word tac in let of_attribute = ("name",tacname)::("script",tac)::of_attribute in (****** le but *) - let {Evd.evar_concl=concl; - Evd.evar_hyps=hyps}=goal in + + let concl = Goal.V82.concl sigma goal in + let hyps = Goal.V82.hyps sigma goal in let env = Global.env_of_context hyps in + let xgoal = X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in @@ -188,14 +185,12 @@ Pp.ppnl (Pp.(++) (Pp.str [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>] end - | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} -> - Util.anomaly "Not Implemented" - | {PT.ref=Some(PT.Daimon,_)} -> X.xml_empty "Hidden_open_goal" of_attribute | {PT.ref=None;PT.goal=goal} -> X.xml_empty "Open_goal" of_attribute + | {PT.ref=Some(PT.Decl_proof _, _)} -> failwith "TODO: xml and decl_proof" in [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ; X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n"); diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml index 344a1581..c854427d 100644 --- a/plugins/xml/unshare.ml +++ b/plugins/xml/unshare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) diff --git a/plugins/xml/unshare.mli b/plugins/xml/unshare.mli index 4b96b22e..cace2de6 100644 --- a/plugins/xml/unshare.mli +++ b/plugins/xml/unshare.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4 index 2d73074b..8a4eb39a 100644 --- a/plugins/xml/xml.ml4 +++ b/plugins/xml/xml.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) diff --git a/plugins/xml/xml.mli b/plugins/xml/xml.mli index ffaad957..0b6d5198 100644 --- a/plugins/xml/xml.mli +++ b/plugins/xml/xml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -12,8 +12,6 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i $Id: xml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* Tokens for XML cdata, empty elements and not-empty elements *) (* Usage: *) (* Str cdata *) diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 7e7f890f..1037bbf0 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -527,8 +527,10 @@ let print internal glob_ref kind xml_library_root = Cic2acic.Variable kn,mk_variable_obj id body typ | Ln.ConstRef kn -> let id = N.id_of_label (N.con_label kn) in - let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = - G.lookup_constant kn in + let cb = G.lookup_constant kn in + let val0 = D.body_of_constant cb in + let typ = cb.D.const_type in + let hyps = cb.D.const_hyps in let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> @@ -557,43 +559,13 @@ let print_ref qid fn = (* where dest is either None (for stdout) or (Some filename) *) (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = - let pf = Tacmach.proof_of_pftreestate pftst in - let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in - let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree, - unshared_pf - = - Proof2aproof.extract_open_pftreestate pftst in - let env = Global.env () in - let obj = - mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in - let uri = - match kind with - Decl_kinds.Local, _ -> - let uri = - "cic:/" ^ String.concat "/" - (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable) - in - let kind_of_var = "VARIABLE","LocalFact" in - (match internal with - | Declare.KernelSilent -> () - | _ -> print_object_kind uri kind_of_var - ); uri - | Decl_kinds.Global, _ -> - let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in - (match internal with - | Declare.KernelSilent -> () - | _ -> print_object_kind uri (kind_of_global_goal kind) - ); uri - in - print_object uri obj evar_map - (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr, - proof_tree_to_flattened_proof_tree)) fn -;; + if true then + Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version." let show fn = let pftst = Pfedit.get_pftreestate () in let (id,kind,_,_) = Pfedit.current_proof_statement () in - show_pftreestate Declare.KernelVerbose fn (kind,pftst) id + show_pftreestate false fn (kind,pftst) id ;; @@ -680,7 +652,7 @@ let _ = end ; Option.iter (fun fn -> - let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) 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 command cmd = if Sys.command cmd <> 0 then diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli index eadf3cfd..ec50d623 100644 --- a/plugins/xml/xmlcommand.mli +++ b/plugins/xml/xmlcommand.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -12,8 +12,6 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i $Id: xmlcommand.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* print_global qid fn *) (* where qid is a long name denoting a definition/theorem or *) (* an inductive definition *) diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index f9d5bac0..d65a1bd3 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -14,8 +14,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: xmlentries.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util;; open Vernacinterp;; |