diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
| commit | 9c6487ba87f448daa28158c6e916e3d932c50645 (patch) | |
| tree | 31bc965d5d14b34d4ab501cbd2350d1de44750c5 /kernel/conv_oracle.ml | |
| parent | 1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff) | |
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/conv_oracle.ml')
| -rw-r--r-- | kernel/conv_oracle.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 11d4435c2..1504220ac 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -9,7 +9,6 @@ (* $Id$ *) open Names -open Closure (* Opaque constants *) let cst_transp = ref KNpred.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 *) - +type transparent_state = Idpred.t * KNpred.t let init() = (cst_transp := KNpred.full; var_transp := Idpred.full) let freeze () = (!var_transp, !cst_transp) let unfreeze (vo,co) = (cst_transp := co; var_transp := vo) |