1 files changed, 24 insertions, 15 deletions
diff --git a/checker/environ.ml b/checker/environ.ml
index 9db0d60e8..bbd043c8e 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -21,7 +21,15 @@ type env = {
     env_globals       : globals;
     env_rel_context   : rel_context;
     env_stratification : stratification;
-    env_imports : Cic.vodigest MPmap.t }
+    env_imports : Cic.vodigest MPmap.t;
+    env_conv_oracle : oracle; }
+
+let empty_oracle = {
+  var_opacity = Id.Map.empty;
+  cst_opacity = Cmap.empty;
+  var_trstate = Id.Pred.empty;
+  cst_trstate = Cpred.empty;
+}
 
 let empty_env = {
   env_globals =
@@ -34,7 +42,8 @@ let empty_env = {
   env_stratification =
   { env_universes = Univ.initial_universes;
     env_engagement = PredicativeSet };
-  env_imports = MPmap.empty }
+  env_imports = MPmap.empty;
+  env_conv_oracle = empty_oracle }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
@@ -51,6 +60,8 @@ let set_engagement (impr_set as c) env =
   { env with env_stratification =
       { env.env_stratification with env_engagement = c } }
 
+let set_oracle env oracle = { env with env_conv_oracle = oracle }
+
 (* Digests *)
 
 let add_digest env dp digest =
@@ -115,7 +126,7 @@ let add_constant kn cs env =
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
 
 (* Constant types *)
 
@@ -137,18 +148,16 @@ exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env (kn,u) =
   let cb = lookup_constant kn env in
-  if cb.const_proj = None then
-    match cb.const_body with
-    | Def l_body -> 
-      let b = force_constr l_body in
-      begin
-        match cb.const_universes with
-        | Monomorphic_const _ -> b
-        | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
-      end
-    | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
-    | Undef _ -> raise (NotEvaluableConst NoBody)
-  else raise (NotEvaluableConst IsProj)
+  match cb.const_body with
+  | Def l_body ->
+    let b = force_constr l_body in
+    begin
+      match cb.const_universes with
+      | Monomorphic_const _ -> b
+      | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+    end
+  | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+  | Undef _ -> raise (NotEvaluableConst NoBody)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =