diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 /kernel/conv_oracle.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/conv_oracle.ml')
| -rw-r--r-- | kernel/conv_oracle.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 1504220ac..d0f5cf63e 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -11,12 +11,12 @@ open Names (* Opaque constants *) -let cst_transp = ref KNpred.full +let cst_transp = ref Cpred.full -let set_opaque_const kn = cst_transp := KNpred.remove kn !cst_transp -let set_transparent_const kn = cst_transp := KNpred.add kn !cst_transp +let set_opaque_const kn = cst_transp := Cpred.remove kn !cst_transp +let set_transparent_const kn = cst_transp := Cpred.add kn !cst_transp -let is_opaque_cst kn = not (KNpred.mem kn !cst_transp) +let is_opaque_cst kn = not (Cpred.mem kn !cst_transp) (* Opaque variables *) let var_transp = ref Idpred.full @@ -36,7 +36,7 @@ let is_opaque = function let oracle_order k1 k2 = is_opaque k2 & not (is_opaque k1) (* summary operations *) -type transparent_state = Idpred.t * KNpred.t -let init() = (cst_transp := KNpred.full; var_transp := Idpred.full) +type transparent_state = Idpred.t * Cpred.t +let init() = (cst_transp := Cpred.full; var_transp := Idpred.full) let freeze () = (!var_transp, !cst_transp) let unfreeze (vo,co) = (cst_transp := co; var_transp := vo) |