diff options
| -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)) |