diff options
| author | Matthieu Sozeau | 2014-07-09 20:06:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-09 20:08:29 +0200 |
| commit | ab5d23b0a82fba784080946f6bb00dd123f64080 (patch) | |
| tree | f3ae7df2b34770c39c62a0249a3537d7b296a73c | |
| parent | 632e7a52e634634d1ba71325b30283dc70ff4b3c (diff) | |
Revert patch making the oracle be used for the transparent state in evarconv,
which made CoRN (and probably Ergo) fail. Another option should be found for
making a constant not unfoldable by tactics/refinement.
| -rw-r--r-- | pretyping/evarconv.ml | 11 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 |
2 files changed, 11 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a9c4c8dc62..ca0644c47e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1068,22 +1068,25 @@ let consider_remaining_unif_problems env exception UnableToUnify of evar_map * unification_error -let the_conv_x env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) t1 t2 evd = +let default_transparent_state env = full_transparent_state +(* Conv_oracle.get_transp_state (Environ.oracle env) *) + +let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = match evar_conv_x ts env evd CONV t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) -let the_conv_x_leq env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) t1 t2 evd = +let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = match evar_conv_x ts env evd CUMUL t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) -let e_conv env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evdref t1 t2 = +let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CONV t1 t2 with | Success evd' -> evdref := evd'; true | _ -> false -let e_cumul env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evdref t1 t2 = +let e_cumul env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CUMUL t1 t2 with | Success evd' -> evdref := evd'; true | _ -> false diff --git a/pretyping/unification.ml b/pretyping/unification.ml index dd0f68390d..b358d6302a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -367,9 +367,11 @@ let subterm_restriction is_subterm flags = let key_of env b flags f = if subterm_restriction b flags then None else match kind_of_term f with - | Const (cst, u) when Cpred.mem cst (snd flags.modulo_delta) -> + | Const (cst, u) when is_transparent env (ConstKey cst) && + Cpred.mem cst (snd flags.modulo_delta) -> Some (IsKey (ConstKey (cst, u))) - | Var id when Id.Pred.mem id (fst flags.modulo_delta) -> + | Var id when is_transparent env (VarKey id) && + Id.Pred.mem id (fst flags.modulo_delta) -> Some (IsKey (VarKey id)) | Proj (p, c) when Cpred.mem p (snd flags.modulo_delta) -> Some (IsProj (p, c)) |