Changeset 1350 for src/common
- Timestamp:
- Oct 11, 2011, 2:27:53 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r1268 r1350 354 354 | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?) 355 355 cases (map_partial … f tl) in IH ⊢ % 356 #x #IH normalize in ⊢ (??%? → ?) #ABS destruct 356 #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize 357 357 >(IH x) // ]] 358 358 qed. … … 486 486 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct 487 487 | #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 // 489 489 >e0 in e1; normalize #H @H ] 490 490 qed.
Note: See TracChangeset
for help on using the changeset viewer.