refined the conversion oracle

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

2 files changed, 16 insertions, 24 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 2f85b18e5..28e121ab2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -26,23 +26,20 @@ let cbv_vm env _ c =
   let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
   Vnorm.cbv_vm env c ctyp
 
-
-let set_opaque_const sp = 
-  Conv_oracle.set_opaque_const sp;
-  Csymtable.set_opaque_const sp
-
-let set_transparent_const sp =
-  let cb = Global.lookup_constant sp in
-  if cb.const_body <> None & cb.const_opaque then
-    errorlabstrm "set_transparent_const"
-      (str "Cannot make" ++ spc () ++ 
-         Nametab.pr_global_env Idset.empty (ConstRef sp) ++
-         spc () ++ str "transparent because it was declared opaque.");
-  Conv_oracle.set_transparent_const sp;
-  Csymtable.set_transparent_const sp
-
-let set_opaque_var      = Conv_oracle.set_opaque_var
-let set_transparent_var = Conv_oracle.set_transparent_var
+let set_strategy k l = 
+  Conv_oracle.set_strategy k l;
+  match k,l with
+      ConstKey sp, Conv_oracle.Opaque ->
+        Csymtable.set_opaque_const sp
+    | ConstKey sp, _ ->
+        let cb = Global.lookup_constant sp in
+        if cb.const_body <> None & cb.const_opaque then
+          errorlabstrm "set_transparent_const"
+            (str "Cannot make" ++ spc () ++ 
+            Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+            spc () ++ str "transparent because it was declared opaque.");
+        Csymtable.set_transparent_const sp
+    | _ -> ()
 
 let _ = 
   Summary.declare_summary "Transparent constants and variables"
@@ -70,7 +67,7 @@ let make_flag f =
   let red =
     if f.rDelta then (* All but rConst *)
         let red = red_add red fDELTA in
-        let red = red_add_transparent red (Conv_oracle.freeze ()) in
+        let red = red_add_transparent red (Conv_oracle.get_transp_state()) in
 	List.fold_right
 	  (fun v red -> red_sub red (make_flag_constant v))
 	  f.rConst red
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index fee3f9813..404a8a196 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -25,13 +25,8 @@ val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
 val declare_red_expr : string -> reduction_function -> unit
 
 (* Opaque and Transparent commands. *)
-val set_opaque_const      : constant -> unit
-val set_transparent_const : constant -> unit
-
-val set_opaque_var      : identifier -> unit
-val set_transparent_var : identifier -> unit
-
 
+val set_strategy : 'a tableKey ->  Conv_oracle.level -> unit
 
 (* call by value normalisation function using the virtual machine *)
 val cbv_vm : reduction_function