From 1f95f087d79d6c2c79012921ce68553caf20b090 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 5 Nov 2002 16:59:16 +0000 Subject: Intégration des modifs de la branche mowgli : - Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/correctness/psyntax.ml4 | 2 +- contrib/correctness/ptactic.ml | 4 ++-- contrib/interface/centaur.ml4 | 2 +- contrib/interface/name_to_ast.ml | 7 ++++--- contrib/interface/xlate.ml | 38 ++++++++++++++------------------------ 5 files changed, 22 insertions(+), 31 deletions(-) (limited to 'contrib') diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 59a32bafb..591076bdd 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -548,7 +548,7 @@ let _ = if not (is_mutable v) then begin let c = Entries.ParameterEntry (trad_ml_type_v ren env v), - Libnames.NeverDischarge in + Decl_kinds.IsAssumption Decl_kinds.Definitional in List.iter (fun id -> ignore (Declare.declare_constant id c)) ids; if_verbose (is_assumed false) ids diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index aac393690..c24baea80 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -17,6 +17,7 @@ open Libnames open Term open Pretyping open Pfedit +open Decl_kinds open Vernacentries open Pmisc @@ -27,7 +28,6 @@ open Prename open Peffect open Pmonad - (* [coqast_of_prog: program -> constr * constr] * Traduction d'un programme impératif en un but (second constr) * et un terme de preuve partiel pour ce but (premier constr) @@ -239,7 +239,7 @@ let correctness s p opttac = let sigma = Evd.empty in let cty = Reduction.nf_betaiota cty in let id = id_of_string s in - start_proof id (false, NeverDischarge) sign cty correctness_hook; + start_proof id (IsGlobal (Proof Lemma)) sign cty correctness_hook; Penv.new_edited id (v,p); if !debug then show_open_subgoals(); deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index b1602655f..b917f24d4 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -417,7 +417,7 @@ let inspect n = oname, Lib.Leaf lobj -> (match oname, object_tag lobj with (sp,_), "VARIABLE" -> - let ((_, _, v), _) = get_variable (basename sp) in + let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), ("CONSTANT"|"PARAMETER") -> let {const_type=typ} = Global.lookup_constant kn in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index ef232d0dc..ec600d21d 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -19,6 +19,7 @@ open Pp;; open Declare;; open Nametab open Vernacexpr;; +open Decl_kinds;; (* This function converts the parameter binders of an inductive definition, in particular you have to be careful to handle each element in the @@ -150,7 +151,7 @@ let make_variable_ast name typ implicits = *) let make_variable_ast name typ implicits = (VernacAssumption - (AssumptionVariable, [false,(name, constr_to_ast (body_of_type typ))])) + ((Local,Definitional), [false,(name, constr_to_ast (body_of_type typ))])) ::(implicits_to_ast_list implicits);; (* @@ -165,7 +166,7 @@ let make_definition_ast name c typ implicits = (implicits_to_ast_list implicits);; *) let make_definition_ast name c typ implicits = - VernacDefinition (Definition, name, DefineBody ([], None, + VernacDefinition (Global, name, DefineBody ([], None, (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), (fun _ _ -> ())) ::(implicits_to_ast_list implicits);; @@ -183,7 +184,7 @@ let constant_to_ast_list kn = make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = - let ((id, c, v), _) = get_variable sp in + let (id, c, v) = get_variable sp in let l = implicits_of_var sp in (match c with None -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 7142f1e6d..92a35b892 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -12,6 +12,7 @@ open Genarg;; open Rawterm;; open Tacexpr;; open Vernacexpr;; +open Decl_kinds;; let in_coq_ref = ref false;; @@ -1467,27 +1468,18 @@ let xlate_thm x = CT_thm (match x with | Theorem -> "Theorem" | Remark -> "Remark" | Lemma -> "Lemma" - | Fact -> "Fact" - | Decl -> "Decl") + | Fact -> "Fact") let xlate_defn x = CT_defn (match x with - | LocalDefinition -> "Local" - | Definition -> "Definition") - - -let xlate_defn_or_thm = - function - (* Unable to decide if a fact in one section or at toplevel, a remark - at toplevel or a theorem or a Definition *) - | StartTheoremProof k -> CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k) - | StartDefinitionBody k -> CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k);; + | Local -> "Local" + | Global -> "Definition") let xlate_var x = CT_var (match x with - | AssumptionParameter -> "Parameter" - | AssumptionAxiom -> "Axiom" - | AssumptionVariable -> "Variable" - | AssumptionHypothesis -> "Hypothesis");; + | (Global,Definitional) -> "Parameter" + | (Global,Logical) -> "Axiom" + | (Local,Definitional) -> "Variable" + | (Local,Logical) -> "Hypothesis");; let xlate_dep = @@ -1915,8 +1907,7 @@ let xlate_vernac = | VernacNotation _ -> xlate_error "TODO: Notation" - | VernacInfix (str_assoc, n, str, id, sc) -> - (* TODO: handle scopes *) + | VernacInfix (str_assoc, n, str, id, None) -> CT_infix ( (match str_assoc with | Some Gramext.LeftA -> CT_lefta @@ -1924,15 +1915,15 @@ let xlate_vernac = | Some Gramext.NonA -> CT_nona | None -> CT_coerce_NONE_to_ASSOC CT_none), CT_int n, CT_string str, loc_qualid_to_ct_ID id) + | VernacInfix _ -> xlate_error "TODO: handle scopes" | VernacGrammar _ -> xlate_error "GRAMMAR not implemented" | VernacCoercion (s, id1, id2, id3) -> let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in let local_opt = match s with (* Cannot decide whether it is a global or a Local but at toplevel *) - | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none - | Libnames.DischargeAt _ -> CT_local - | Libnames.NotDeclare -> assert false in + | Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none + | Local -> CT_local in CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1, xlate_class id2, xlate_class id3) @@ -1941,9 +1932,8 @@ let xlate_vernac = let local_opt = match s with (* Cannot decide whether it is a global or a Local but at toplevel *) - | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none - | Libnames.DischargeAt _ -> CT_local - | Libnames.NotDeclare -> assert false in + | Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none + | Local -> CT_local in CT_coercion (local_opt, id_opt, xlate_ident id1, xlate_class id2, xlate_class id3) | VernacResetName id -> CT_reset (xlate_ident id) -- cgit v1.2.3