diff options
| author | herbelin | 2006-01-28 23:07:59 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-28 23:07:59 +0000 |
| commit | 35180e3a927d4450406ebeb0e89fdcde1341650a (patch) | |
| tree | 7fe926a33569320b25c1fa972904354b067061ea /library | |
| parent | adadd8db0e9eb1e5161057a7064426b84a3d2605 (diff) | |
Réorganisation de la structure interne des types de déclarations (decl_kinds)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 8 | ||||
| -rw-r--r-- | library/declare.mli | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/library/declare.ml b/library/declare.ml index 5359290be4..3835180b16 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -59,14 +59,14 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types -type variable_declaration = dir_path * section_variable_entry * local_kind +type variable_declaration = dir_path * section_variable_entry * logical_kind type checked_section_variable = | CheckedSectionLocalDef of constr * types * Univ.constraints * bool | CheckedSectionLocalAssum of types * Univ.constraints type checked_variable_declaration = - dir_path * checked_section_variable * local_kind + dir_path * checked_section_variable * logical_kind let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t) @@ -123,9 +123,9 @@ let declare_variable id obj = (* Globals: constants and parameters *) -type constant_declaration = constant_entry * global_kind +type constant_declaration = constant_entry * logical_kind -let csttab = ref (Spmap.empty : global_kind Spmap.t) +let csttab = ref (Spmap.empty : logical_kind Spmap.t) let _ = Summary.declare_summary "CONSTANT" { Summary.freeze_function = (fun () -> !csttab); diff --git a/library/declare.mli b/library/declare.mli index 317c27281f..f04170b34e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -36,14 +36,14 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types -type variable_declaration = dir_path * section_variable_entry * local_kind +type variable_declaration = dir_path * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> object_name (* Declaration of global constructions *) (* i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = constant_entry * global_kind +type constant_declaration = constant_entry * logical_kind (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -66,11 +66,11 @@ val string_of_strength : strength -> string val is_constant : section_path -> bool val constant_strength : section_path -> strength -val constant_kind : section_path -> global_kind +val constant_kind : section_path -> logical_kind val get_variable : variable -> named_declaration val variable_strength : variable -> strength -val variable_kind : variable -> local_kind +val variable_kind : variable -> logical_kind val find_section_variable : variable -> section_path val last_section_hyps : dir_path -> identifier list val clear_proofs : named_context -> Environ.named_context_val |