Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 10 deletions

diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 350e1a5a0..ffa7735e7 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -12,36 +12,36 @@ open Names
 open Closure
 
 (* Opaque constants *)
-let cst_transp = ref Sppred.full
+let cst_transp = ref KNpred.full
 
-let set_opaque_const sp = cst_transp := Sppred.remove sp !cst_transp
-let set_transparent_const sp = cst_transp := Sppred.add sp !cst_transp
+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 is_opaque_cst sp = not (Sppred.mem sp !cst_transp)
+let is_opaque_cst kn = not (KNpred.mem kn !cst_transp)
 
 (* Unfold the first only if it is not opaque and the second is
    opaque *)
-let const_order sp1 sp2 = is_opaque_cst sp2 & not (is_opaque_cst sp1)
+let const_order kn1 kn2 = is_opaque_cst kn2 & not (is_opaque_cst kn1)
 
 (* Opaque variables *)
 let var_transp = ref Idpred.full
 
-let set_opaque_var sp = var_transp := Idpred.remove sp !var_transp
-let set_transparent_var sp = var_transp := Idpred.add sp !var_transp
+let set_opaque_var kn = var_transp := Idpred.remove kn !var_transp
+let set_transparent_var kn = var_transp := Idpred.add kn !var_transp
 
-let is_opaque_var sp = not (Idpred.mem sp !var_transp)
+let is_opaque_var kn = not (Idpred.mem kn !var_transp)
 
 let var_order id1 id2 = is_opaque_var id2 & not (is_opaque_var id1)
 
 (* *)
 let oracle_order k1 k2 =
   match (k1,k2) with
-      (ConstKey sp1, ConstKey sp2) -> const_order sp1 sp2
+      (ConstKey kn1, ConstKey kn2) -> const_order kn1 kn2
     | (VarKey id1, VarKey id2) -> var_order id1 id2
     | _ -> false
 
 (* summary operations *)
 
-let init() = (cst_transp := Sppred.full; var_transp := Idpred.full)
+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)