aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-16 12:37:40 +0000
committerGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-16 12:37:40 +0000
commitd6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch)
treeed4d954a685588ee55f4d8902eba8a1afc864472 /interp
parent08cb37edb71af0301a72acc834d50f24b0733db5 (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 'interp')
-rw-r--r--interp/constrextern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 77853ade8..87cc59b8f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -114,7 +114,7 @@ let extern_evar loc n =
let raw_string_of_ref = function
| ConstRef kn ->
- "CONST("^(string_of_kn kn)^")"
+ "CONST("^(string_of_con kn)^")"
| IndRef (kn,i) ->
"IND("^(string_of_kn kn)^","^(string_of_int i)^")"
| ConstructRef ((kn,i),j) ->