Conv_orable made functional and part of pre_env

But for vm, the kernel should be functional now

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

4 files changed, 13 insertions, 11 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8a614d65fd..41bd33dbcf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -748,9 +748,10 @@ 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 = match Conv_oracle.get_strategy k with
-| Conv_oracle.Opaque -> false
-| _ -> true
+let is_transparent e k =
+  match Conv_oracle.get_strategy (Environ.oracle e) k with
+  | Conv_oracle.Opaque -> false
+  | _ -> true
 
 (* Conversion utility functions *)
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 6640392063..cd3ed1f2f3 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -204,7 +204,7 @@ val contract_fix : ?env:Environ.env -> fixpoint ->
 val fix_recarg : fixpoint -> constr stack -> (int * constr) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
-val is_transparent : 'a tableKey -> bool
+val is_transparent : Environ.env -> 'a tableKey -> bool
 
 (** {6 Conversion Functions (uses closures, lazy strategy) } *)
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index e49f88128c..d6ad76f3e2 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -43,10 +43,10 @@ let error_not_evaluable r =
      spc () ++ str "to an evaluable reference.")
 
 let is_evaluable_const env cst =
-  is_transparent (ConstKey cst) && evaluable_constant cst env
+  is_transparent env (ConstKey cst) && evaluable_constant cst env
 
 let is_evaluable_var env id =
-  is_transparent (VarKey id) && evaluable_named id env
+  is_transparent env (VarKey id) && evaluable_named id env
 
 let is_evaluable env = function
   | EvalConstRef cst -> is_evaluable_const env cst
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9c21446da4..4189741baa 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -323,13 +323,13 @@ let expand_key env = function
 let subterm_restriction is_subterm flags =
   not is_subterm && flags.restrict_conv_on_strict_subterms
 
-let key_of b flags f =
+let key_of env b flags f =
   if subterm_restriction b flags then None else
   match kind_of_term f with
-  | Const cst when is_transparent (ConstKey cst) &&
+  | Const cst when is_transparent env (ConstKey cst) &&
         Cpred.mem cst (snd flags.modulo_delta) ->
       Some (ConstKey cst)
-  | Var id when is_transparent (VarKey id) &&
+  | Var id when is_transparent env (VarKey id) &&
         Id.Pred.mem id (fst flags.modulo_delta) ->
       Some (VarKey id)
   | _ -> None
@@ -343,7 +343,8 @@ let oracle_order env cf1 cf2 =
   | Some k1 ->
       match cf2 with
       | None -> Some true
-      | Some k2 -> Some (Conv_oracle.oracle_order false k1 k2)
+      | Some k2 ->
+          Some (Conv_oracle.oracle_order (Environ.oracle env) false k1 k2)
 
 let do_reduce ts (env, nb) sigma c =
   zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, empty_stack)))
@@ -567,7 +568,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
     then
       substn
     else
-      let cf1 = key_of b flags f1 and cf2 = key_of b flags f2 in
+      let cf1 = key_of env b flags f1 and cf2 = key_of env b flags f2 in
 	match oracle_order curenv cf1 cf2 with
 	| None -> error_cannot_unify curenv sigma (cM,cN)
 	| Some true ->