From d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f Mon Sep 17 00:00:00 2001 From: sacerdot Date: Tue, 16 Nov 2004 12:37:40 +0000 Subject: 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 --- kernel/cemitcodes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 421949163..1b93dc4b6 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -254,7 +254,7 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_kn s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.map (subst_patch s) pl,fv @@ -265,7 +265,7 @@ type body_code = let subst_body_code s = function | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) - | BCallias kn -> BCallias (subst_kn s kn) + | BCallias kn -> BCallias (subst_con s kn) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted -- cgit v1.2.3