Changeset 1350 for src/common


Ignore:
Timestamp:
Oct 11, 2011, 2:27:53 AM (8 years ago)
Author:
sacerdot
Message:

Porting to latest destruct tactic.

Note: the tactics has a few remaining bugs to be ironed out.
Look for "Wilmer: XXX" comments in the .ma files to see where
these are avoided ATM using axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1268 r1350  
    354354    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
    355355      cases (map_partial … f tl) in IH ⊢ %
    356       #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
     356      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize
    357357      >(IH x) // ]]
    358358qed.
     
    486486 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
    487487 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
    488    #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
     488   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ % >e0 //
    489489   >e0 in e1; normalize #H @H ]
    490490qed.
Note: See TracChangeset for help on using the changeset viewer.