From dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 31 Oct 2013 14:24:43 +0000
Subject: 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
---
 pretyping/unification.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'pretyping/unification.ml')

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 ->
-- 
cgit v1.2.3