diff options
| -rw-r--r-- | contrib/field/Field_Tactic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v index 0ae9db996..de8efbb39 100644 --- a/contrib/field/Field_Tactic.v +++ b/contrib/field/Field_Tactic.v @@ -177,8 +177,8 @@ Tactic Definition Multiply mul := [Intro; Let id = GrepMult In Apply (mult_eq ?1 ?3 ?4 mul ?2 id)(*; - Cbv Beta Delta -[interp_ExprA] Iota*) - |Cbv Beta Delta -[not] Iota; + Cbv Beta Delta -[interp_ExprA] Zeta Evar Iota*) + |Cbv Beta Delta -[not] Zeta Evar Iota; Let AmultT = Eval Compute in (Amult ?1) And AoneT = Eval Compute in (Aone ?1) In (Match Context With |