diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 /library/declare.mli | |
| parent | 08cb37edb71af0301a72acc834d50f24b0733db5 (diff) | |
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/library/declare.mli b/library/declare.mli index a025982ee..6af513888 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -52,10 +52,11 @@ type constant_declaration = constant_entry * global_kind (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) -val declare_constant : identifier -> constant_declaration -> object_name +val declare_constant : + identifier -> constant_declaration -> constant val declare_internal_constant : - identifier -> constant_declaration -> object_name + identifier -> constant_declaration -> constant val redeclare_constant : identifier -> Dischargedhypsmap.discharged_hyps -> @@ -98,5 +99,5 @@ val strength_of_global : global_reference -> strength (* hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit -val set_xml_declare_constant : (bool * object_name -> unit) -> unit +val set_xml_declare_constant : (bool * constant -> unit) -> unit val set_xml_declare_inductive : (bool * object_name -> unit) -> unit |