diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /kernel/conv_oracle.ml | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'kernel/conv_oracle.ml')
| -rw-r--r-- | kernel/conv_oracle.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index dba373ce..4c692308 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -6,18 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: conv_oracle.ml,v 1.2.8.2 2004/07/16 19:30:24 herbelin Exp $ *) +(* $Id: conv_oracle.ml 6303 2004-11-16 12:37:40Z sacerdot $ *) open Names -open Closure (* 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 @@ -31,13 +30,13 @@ let is_opaque_var kn = not (Idpred.mem kn !var_transp) let is_opaque = function | ConstKey cst -> is_opaque_cst cst | VarKey id -> is_opaque_var id - | FarRelKey _ -> false + | RelKey _ -> false (* Unfold the first only if it is not opaque and the second is opaque *) let oracle_order k1 k2 = is_opaque k2 & not (is_opaque k1) (* summary operations *) - -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) |