diff options
| author | sacerdot | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 /parsing/prettyp.ml | |
| 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 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f84aa664b8..e308230782 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -363,7 +363,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = | (_,"VARIABLE") -> Some (print_section_variable (basename sp)) | (_,"CONSTANT") -> - Some (print_constant with_values sep kn) + Some (print_constant with_values sep (constant_of_kn kn)) | (_,"INDUCTIVE") -> Some (print_inductive kn) | (_,"MODULE") -> @@ -552,7 +552,7 @@ let print_local_context () = | (oname,Lib.Leaf lobj)::rest -> (match object_tag lobj with | "CONSTANT" -> - let kn = snd oname in + let kn = constant_of_kn (snd oname) in let {const_body=val_0;const_type=typ} = Global.lookup_constant kn in (print_last_const rest ++ |