diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 94468e6dc2..a6de33ace4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -136,10 +136,13 @@ let default_no_delta_unify_flags = { } let expand_constant env flags c = - let (ids,csts) = Conv_oracle.freeze() in match kind_of_term c with - | Const cst when Cpred.mem cst csts && Cpred.mem cst (snd flags.modulo_delta) -> constant_opt_value env cst - | Var id when Idpred.mem id ids && Idpred.mem id (fst flags.modulo_delta) -> named_body id env + | Const cst when is_transparent (ConstKey cst) && + Cpred.mem cst (snd flags.modulo_delta) -> + constant_opt_value env cst + | Var id when is_transparent (VarKey id) && + Idpred.mem id (fst flags.modulo_delta) -> + named_body id env | _ -> None let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = |