diff options
Diffstat (limited to 'contrib/field/Field_Tactic.v')
| -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 5bc4e4433..00f0cbe89 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] Zeta Evar Iota*) - |Cbv Beta Delta -[not] Zeta Evar Iota; + Cbv Beta Delta -[interp_ExprA] Zeta Iota*) + |Cbv Beta Delta -[not] Zeta Iota; Let AmultT = Eval Compute in (Amult ?1) And AoneT = Eval Compute in (Aone ?1) In (Match Context With |