Ignore:
Timestamp:
Oct 19, 2011, 11:54:13 AM (9 years ago)
Author:
campbell
Message:

Remove a few old workarounds.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r1369 r1410  
    145145  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?) %
    146146  | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
    147     [ whd in ⊢ (??%? → ?) #E'
    148       (* XXX need to normalize or destruct is intractable *)
    149       normalize in E'; destruct (E') ; %
     147    [ whd in ⊢ (??%? → ?) #E' destruct; %
    150148    | #b #c #o whd in ⊢ (??%? → ?) #E' destruct %
    151149    ]
Note: See TracChangeset for help on using the changeset viewer.