diff options
| author | gareuselesinge | 2013-10-31 14:24:43 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-31 14:24:43 +0000 |
| commit | dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e (patch) | |
| tree | f09931dac187ca9b20bb483aee7bc9beca1e78f1 /pretyping/unification.ml | |
| parent | b0631cba10fda88eb3518153860807b10441ef34 (diff) | |
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
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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 -> |