28 files changed, 96 insertions, 69 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 1fc249eef..c14d72def 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -60,13 +60,13 @@ Future
 Lazyconstr
 Declareops
 Retroknowledge
+Conv_oracle
 Pre_env
 Nativelambda
 Nativecode
 Nativelib
 Cbytegen
 Environ
-Conv_oracle
 Closure
 Reduction
 Nativeconv
diff --git a/kernel/closure.ml b/kernel/closure.ml
index db57503f6..187ea4478 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -1007,5 +1007,6 @@ type clos_infos = fconstr infos
 
 let create_clos_infos ?(evars=fun _ -> None) flgs env =
   create (fun _ -> inject) flgs env evars
+let oracle_of_infos { i_env } = Environ.oracle i_env
 
 let unfold_reference = ref_value_cache
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 3a9603a37..161de91cf 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -163,6 +163,7 @@ val destFLambda :
 type clos_infos
 val create_clos_infos :
   ?evars:(existential->constr option) -> reds -> env -> clos_infos
+val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
 (** Reduction function *)
 
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 65efb4fd0..32aaacb62 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -26,48 +26,46 @@ let is_transparent = function
 | Level 0 -> true
 | _ -> false
 
-type oracle = level Id.Map.t * level Cmap.t
+type oracle = {
+  var_opacity : level Id.Map.t;
+  cst_opacity : level Cmap.t
+}
 
-let var_opacity = ref Id.Map.empty
-let cst_opacity = ref Cmap.empty
+let empty = { var_opacity = Id.Map.empty; cst_opacity = Cmap.empty }
 
-(* summary operations *)
-let freeze _ = (!var_opacity, !cst_opacity)
-let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)
-
-let get_strategy = function
+let get_strategy { var_opacity; cst_opacity } = function
   | VarKey id ->
-      (try Id.Map.find id !var_opacity
+      (try Id.Map.find id var_opacity
       with Not_found -> default)
   | ConstKey c ->
-      (try Cmap.find c !cst_opacity
+      (try Cmap.find c cst_opacity
       with Not_found -> default)
   | RelKey _ -> Expand
 
-let set_strategy k l =
+let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
   match k with
   | VarKey id ->
-      var_opacity :=
-      if is_default l then Id.Map.remove id !var_opacity
-      else Id.Map.add id l !var_opacity
+      { oracle with var_opacity =
+          if is_default l then Id.Map.remove id var_opacity
+          else Id.Map.add id l var_opacity }
   | ConstKey c ->
-      cst_opacity :=
-      if is_default l then Cmap.remove c !cst_opacity
-      else Cmap.add c l !cst_opacity
+      { oracle with cst_opacity =
+          if is_default l then Cmap.remove c cst_opacity
+          else Cmap.add c l cst_opacity }
   | RelKey _ -> Errors.error "set_strategy: RelKey"
 
-let get_transp_state () =
+let get_transp_state { var_opacity; cst_opacity } =
   (Id.Map.fold
     (fun id l ts -> if  l=Opaque then Id.Pred.remove id ts else ts)
-    !var_opacity Id.Pred.full,
+    var_opacity Id.Pred.full,
    Cmap.fold
     (fun c l ts -> if  l=Opaque then Cpred.remove c ts else ts)
-    !cst_opacity Cpred.full)
+    cst_opacity Cpred.full)
 
 (* Unfold the first constant only if it is "more transparent" than the
    second one. In case of tie, expand the second one. *)
-let oracle_order l2r k1 k2 =
-  match get_strategy k1, get_strategy k2 with
+let oracle_order o l2r k1 k2 =
+  match get_strategy o k1, get_strategy o k2 with
     | Expand, _ -> true
     | Level n1, Opaque -> true
     | Level n1, Level n2 -> n1 < n2
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 7bb62112c..24797238d 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -8,11 +8,15 @@
 
 open Names
 
+type oracle
+
+val empty : oracle
+
 (** Order on section paths for unfolding.
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
+val oracle_order : oracle -> bool -> 'a tableKey -> 'a tableKey -> bool
 
 (** Priority for the expansion of constant in the conversion test.
  * Higher levels means that the expansion is less prioritary.
@@ -25,16 +29,11 @@ val transparent : level
 (** Check whether a level is transparent *)
 val is_transparent : level -> bool
 
-val get_strategy : 'a tableKey -> level
+val get_strategy : oracle -> 'a tableKey -> level
 
 (** Sets the level of a constant.
  * Level of RelKey constant cannot be set. *)
-val set_strategy : 'a tableKey -> level -> unit
+val set_strategy : oracle -> 'a tableKey -> level -> oracle
 
-val get_transp_state : unit -> transparent_state
+val get_transp_state : oracle -> transparent_state
 
-(****************************
-   Summary operations *)
-type oracle
-val freeze   : [ `Yes | `No | `Shallow ] -> oracle
-val unfreeze : oracle -> unit
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ae6817a76..9f1868004 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -38,6 +38,8 @@ type env = Pre_env.env
 
 let pre_env env = env
 let env_of_pre_env env = env
+let oracle env = env.env_conv_oracle
+let set_oracle env o = { env with env_conv_oracle = o }
 
 let empty_named_context_val = empty_named_context_val
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index d378501a0..38a1bf68a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -32,6 +32,8 @@ open Declarations
 type env
 val pre_env : env -> Pre_env.env
 val env_of_pre_env : Pre_env.env -> env
+val oracle : env -> Conv_oracle.oracle
+val set_oracle : env -> Conv_oracle.oracle -> env
 
 type named_context_val
 val eq_named_context_val : named_context_val -> named_context_val -> bool
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index cbc147e9e..7d318add5 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,13 +15,13 @@ Nativevalues
 Lazyconstr
 Declareops
 Retroknowledge
+Conv_oracle
 Pre_env
 Cbytegen
 Nativelambda
 Nativecode
 Nativelib
 Environ
-Conv_oracle
 Closure
 Reduction
 Nativeconv
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 9a2bb73d1..e543c4e68 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -54,6 +54,7 @@ type env = {
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
   env_stratification : stratification;
+  env_conv_oracle   : Conv_oracle.oracle;
   retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
@@ -74,6 +75,7 @@ let empty_env = {
   env_stratification = {
     env_universes = initial_universes;
     env_engagement = None };
+  env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge }
 
 
@@ -118,6 +120,7 @@ let push_named d env =
     env_rel_val = env.env_rel_val;
     env_nb_rel = env.env_nb_rel;
     env_stratification = env.env_stratification;
+    env_conv_oracle = env.env_conv_oracle;
     retroknowledge = env.retroknowledge; }
 
 let lookup_named_val id env =
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 10c9c27cb..f634719f9 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -46,6 +46,7 @@ type env = {
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
     env_stratification : stratification;
+    env_conv_oracle   : Conv_oracle.oracle;
     retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 48c63ac96..194b223bb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -299,7 +299,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         with NotConvertible ->
           (* else the oracle tells which constant is to be expanded *)
           let (app1,app2) =
-            if Conv_oracle.oracle_order l2r fl1 fl2 then
+            if Conv_oracle.oracle_order (Closure.oracle_of_infos (snd infos)) l2r fl1 fl2 then
               match unfold_reference infos fl1 with
                 | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
                 | None ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 40f16a6e6..3132d45e3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -777,3 +777,7 @@ environment, and store for the future (instead of just its type)
 loaded by side-effect once and for all (like it is done in OCaml).
 Would this be correct with respect to undo's and stuff ?
 *)
+
+let set_strategy e k l = { e with env =
+   (Environ.set_oracle e.env
+      (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b16d5b63d..dcdb866bf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -155,3 +155,6 @@ val register :
   field -> Retroknowledge.entry -> Term.constr -> safe_transformer0
 
 val register_inline : constant -> safe_transformer0
+
+val set_strategy :
+  safe_environment -> 'a Names.tableKey -> Conv_oracle.level -> safe_environment
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 7044b1372..4273596d9 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -99,7 +99,7 @@ and conv_atom pb k a1 stk1 a2 stk2 cu =
 	    conv_stack k stk1 stk2 cu
 	  else raise NotConvertible
 	with NotConvertible ->
-	  if oracle_order false ik1 ik2 then
+	  if oracle_order (oracle_of_infos !infos) false ik1 ik2 then
             conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
           else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
       end
@@ -219,10 +219,10 @@ and conv_eq_vect vt1 vt2 cu =
   else raise NotConvertible
 
 let vconv pb env t1 t2 =
+  infos := create_clos_infos betaiotazeta env;
   let cu =
     try conv_eq pb t1 t2 empty_constraint
     with NotConvertible ->
-      infos := create_clos_infos betaiotazeta env;
       let v1 = val_of_constr env t1 in
       let v2 = val_of_constr env t2 in
       let cu = conv_val pb (nb_rel env) v1 v2 empty_constraint in
diff --git a/library/global.ml b/library/global.ml
index 3b0e504d8..dac840ddb 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -158,3 +158,6 @@ let register field value by_clause =
   globalize0 (Safe_typing.register field (kind_of_term value) by_clause)
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
+
+let set_strategy k l =
+  GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
diff --git a/library/global.mli b/library/global.mli
index c62f51e16..856956a17 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -105,3 +105,8 @@ val register :
   Retroknowledge.field -> Term.constr -> Term.constr -> unit
 
 val register_inline : constant -> unit
+
+(** {6 Oracle } *)
+
+val set_strategy : 'a Names.tableKey -> Conv_oracle.level -> unit
+
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8a614d65f..41bd33dbc 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 664039206..cd3ed1f2f 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 e49f88128..d6ad76f3e 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 9c21446da..4189741ba 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 ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index dba047aa7..0d279c73b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -196,14 +196,16 @@ type opacity =
 
 let opacity env = function
   | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) ->
-      Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v)))
+      Some(TransparentMaybeOpacified
+        (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v)))
   | ConstRef cst ->
       let cb = Environ.lookup_constant cst env in
       (match cb.const_body with
 	| Undef _ -> None
 	| OpaqueDef _ -> Some FullyOpaque
 	| Def _ -> Some
-          (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst))))
+          (TransparentMaybeOpacified
+            (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst))))
   | _ -> None
 
 let print_opacity ref =
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 80d0ead96..69ff1dc51 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -36,7 +36,7 @@ let set_strategy_one ref l  =
     match ref with
       | EvalConstRef sp -> ConstKey sp
       | EvalVarRef id -> VarKey id in
-  Conv_oracle.set_strategy k l;
+  Global.set_strategy k l;
   match k,l with
       ConstKey sp, Conv_oracle.Opaque ->
         Csymtable.set_opaque_const sp
@@ -105,12 +105,6 @@ let inStrategy : strategy_obj -> obj =
 let set_strategy local str =
   Lib.add_anonymous_leaf (inStrategy (local,str))
 
-let _ = Summary.declare_summary "Transparent constants and variables"
-  { Summary.freeze_function = Conv_oracle.freeze;
-    Summary.unfreeze_function = Conv_oracle.unfreeze;
-    Summary.init_function = Summary.nop }
-
-
 (* Generic reduction: reduction functions used in reduction tactics *)
 
 type red_expr =
@@ -120,7 +114,7 @@ let make_flag_constant = function
   | EvalVarRef id -> fVAR id
   | EvalConstRef sp -> fCONST sp
 
-let make_flag f =
+let make_flag env f =
   let red = no_red in
   let red = if f.rBeta then red_add red fBETA else red in
   let red = if f.rIota then red_add red fIOTA else red in
@@ -128,7 +122,8 @@ 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.get_transp_state()) in
+        let red = red_add_transparent red 
+                    (Conv_oracle.get_transp_state (Environ.oracle env)) in
 	List.fold_right
 	  (fun v red -> red_sub red (make_flag_constant v))
 	  f.rConst red
@@ -175,7 +170,9 @@ let out_arg = function
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
-let rec reduction_of_red_expr = function
+let reduction_of_red_expr env =
+  let make_flag = make_flag env in
+  let rec reduction_of_red_expr = function
   | Red internal ->
       if internal then (try_red_product,DEFAULTcast)
       else (red_product,DEFAULTcast)
@@ -218,6 +215,8 @@ let rec reduction_of_red_expr = function
     let redfun = contextually b lp nativefun in
     (redfun, NATIVEcast)
   | CbvNative None -> (cbv_native, NATIVEcast)
+  in
+    reduction_of_red_expr
 
 let subst_flags subs flags =
   { flags with rConst = List.map subs flags.rConst }
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 8a7fcb3c7..31affc280 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -17,10 +17,11 @@ open Locus
 
 type red_expr =
     (constr, evaluable_global_reference, constr_pattern) red_expr_gen
-
+ 
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
-val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
+val reduction_of_red_expr :
+  Environ.env -> red_expr -> reduction_function * cast_kind
 
 (** [true] if we should use the vm to verify the reduction *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 84553e9eb..b8f065b41 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,7 +75,7 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 let pf_parse_const gls = compose (pf_global gls) Id.of_string
 
 let pf_reduction_of_red_expr gls re c =
-  (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c
+  (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_reduce = pf_apply
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index eb7b28690..d6ad598c5 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1048,8 +1048,8 @@ module Strategies =
 	lemmas rewrite_unif_flags lems state env avoid t ty cstr evars
 
     let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
-      let rfn, ckind = Redexpr.reduction_of_red_expr r in
-	fun state env avoid t ty cstr evars ->
+      fun state env avoid t ty cstr evars ->
+        let rfn, ckind = Redexpr.reduction_of_red_expr env r in
 	  let t' = rfn env (goalevars evars) t in
 	    if eq_constr t' t then
 	      state, Some None
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c1bd8e0c9..004a93ed1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -379,7 +379,8 @@ let reduce redexp cl goal =
   let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
   let redexps = reduction_clause redexp cl in
   let tac = tclMAP (fun (where,redexp) ->
-    reduct_option (Redexpr.reduction_of_red_expr redexp) where) redexps in
+    reduct_option
+      (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
   match redexp with
   | Fold _ | Pattern _ -> with_check tac goal
   | _ -> tac goal
@@ -552,7 +553,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
     match pf_lookup_hypothesis_as_renamed env ccl h with
       | None when red ->
           aux
-	    ((fst (Redexpr.reduction_of_red_expr (Red true)))
+	    ((fst (Redexpr.reduction_of_red_expr env (Red true)))
 	       env (project gl) ccl)
       | x -> x
   in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3017aeacb..04a2661d7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -70,7 +70,7 @@ let red_constant_entry n ce = function
       let proof_out = ce.const_entry_body in
       { ce with const_entry_body = Future.chain proof_out (fun (body,eff) ->
           under_binders (Global.env()) 
-            (fst (reduction_of_red_expr red)) n body,eff) }
+            (fst (reduction_of_red_expr (Global.env()) red)) n body,eff) }
 
 let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3c104f543..9ee91815e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1350,7 +1350,7 @@ let vernac_check_may_eval redexp glopt rc =
     | Some r ->
         Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
-	let redfun = fst (reduction_of_red_expr r_interp) in
+	let redfun = fst (reduction_of_red_expr env r_interp) in
 	msg_notice (print_eval redfun env sigma' rc j)
 
 let vernac_declare_reduction locality s r =
@@ -1413,7 +1413,7 @@ let vernac_print = function
   | PrintAssumptions (o,t,r) ->
       (* Prints all the axioms and section variables used by a term *)
       let cstr = constr_of_global (smart_global r) in
-      let st = Conv_oracle.get_transp_state () in
+      let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
       let nassums =
 	Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in
       msg_notice (Printer.pr_assumptionset (Global.env ()) nassums)