refined the conversion oracle

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

4 files changed, 14 insertions, 7 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 55b82e2148..5f5b47783a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -601,6 +601,9 @@ let fakey = Profile.declare_profile "fhnf_apply";;
 let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
 *)
 
+let is_transparent k =
+  Conv_oracle.get_strategy k <> Conv_oracle.Opaque
+
 (* Conversion utility functions *)
 
 type conversion_test = constraints -> constraints
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7968e0db40..c9b157efd9 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -190,6 +190,9 @@ val fix_recarg : fixpoint -> constr stack -> (int * constr) option
 val reduce_fix : local_state_reduction_function -> fixpoint
    -> constr stack -> fix_reduction_result
 
+(*s Querying the kernel conversion oracle: opaque/transparent constants *)
+val is_transparent : 'a tableKey -> bool
+
 (*s Conversion Functions (uses closures, lazy strategy) *)
 
 type conversion_test = constraints -> constraints
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3b50387667..05d1086731 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -38,13 +38,11 @@ exception Redelimination
 let is_evaluable env ref =
   match ref with
       EvalConstRef kn ->
-        let (ids,kns) = Conv_oracle.freeze() in
-        Cpred.mem kn kns &
+        is_transparent (ConstKey kn) &&
         let cb = Environ.lookup_constant kn env in
         cb.const_body <> None & not cb.const_opaque
     | EvalVarRef id ->
-        let (ids,sps) = Conv_oracle.freeze() in
-        Idpred.mem id ids &
+        is_transparent (VarKey id) &&
         let (_,value,_) = Environ.lookup_named id env in
         value <> None
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 94468e6dc2..a6de33ace4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -136,10 +136,13 @@ let default_no_delta_unify_flags = {
 }
 
 let expand_constant env flags c = 
-  let (ids,csts) = Conv_oracle.freeze() in
   match kind_of_term c with
-  | Const cst when Cpred.mem cst csts && Cpred.mem cst (snd flags.modulo_delta) -> constant_opt_value env cst
-  | Var id when Idpred.mem id ids && Idpred.mem id (fst flags.modulo_delta) -> named_body id env
+  | Const cst when is_transparent (ConstKey cst) &&
+                   Cpred.mem cst (snd flags.modulo_delta) ->
+      constant_opt_value env cst
+  | Var id when is_transparent (VarKey id) &&
+                Idpred.mem id (fst flags.modulo_delta) ->
+      named_body id env
   | _ -> None
 
 let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =