Changeset 881 for src/common
- Timestamp:
- Jun 3, 2011, 5:35:31 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r880 r881 479 479 intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence. 480 480 Qed. 481 *) 481 *)*) 482 482 (* * * External functions *) 483 483 … … 532 532 End TRANSF_PARTIAL_FUNDEF. 533 533 *) 534 *) 534 535 535 536 536
Note: See TracChangeset
for help on using the changeset viewer.