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 /kernel/csymtable.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 'kernel/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 402a0fb97b..f9f03e3486 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -55,9 +55,9 @@ let num_boxed = ref 0 let boxed_tbl = Hashtbl.create 53 -let cst_opaque = ref KNpred.full +let cst_opaque = ref Cpred.full -let is_opaque kn = KNpred.mem kn !cst_opaque +let is_opaque kn = Cpred.mem kn !cst_opaque let set_global_boxed kn v = let n = !num_boxed in @@ -163,12 +163,12 @@ and val_of_constr env c = eval_to_patch env (to_memory ccfv) let set_transparent_const kn = - cst_opaque := KNpred.remove kn !cst_opaque; + cst_opaque := Cpred.remove kn !cst_opaque; List.iter (fun n -> (global_boxed()).(n) <- false) (Hashtbl.find_all boxed_tbl kn) let set_opaque_const kn = - cst_opaque := KNpred.add kn !cst_opaque; + cst_opaque := Cpred.add kn !cst_opaque; List.iter (fun n -> (global_boxed()).(n) <- true) (Hashtbl.find_all boxed_tbl kn) |