diff options
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) |