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 /pretyping/termops.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 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d89d5a879c..d4e23af28d 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -35,6 +35,7 @@ let pr_name = function | Anonymous -> str "_" let pr_sp sp = str(string_of_kn sp) +let pr_con sp = str(string_of_con sp) let rec pr_constr c = match kind_of_term c with | Rel n -> str "#"++int n @@ -63,7 +64,7 @@ let rec pr_constr c = match kind_of_term c with | Evar (e,l) -> hov 1 (str"Evar#" ++ int e ++ str"{" ++ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") - | Const c -> str"Cst(" ++ pr_sp c ++ str")" + | Const c -> str"Cst(" ++ pr_con c ++ str")" | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")" | Construct ((sp,i),j) -> str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" @@ -691,7 +692,7 @@ let hdchar env c = | Cast (c,_) -> hdrec k c | App (f,l) -> hdrec k f | Const kn -> - let c = lowercase_first_char (id_of_label (label kn)) in + let c = lowercase_first_char (id_of_label (con_label kn)) in if c = "?" then "y" else c | Ind ((kn,i) as x) -> if i=0 then @@ -799,7 +800,6 @@ let rec is_imported_modpath = function let is_imported_ref = function | VarRef _ -> false - | ConstRef kn | IndRef (kn,_) | ConstructRef ((kn,_),_) (* | ModTypeRef ln *) -> @@ -807,6 +807,8 @@ let is_imported_ref = function (* | ModRef mp -> is_imported_modpath mp *) + | ConstRef kn -> + let (mp,_,_) = repr_con kn in is_imported_modpath mp let is_global id = try |