aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Compat
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-01-21 01:43:10 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-01-21 09:29:26 +0100
commit9c2662eecc398f38be3b6280a8f760cc439bc31c (patch)
tree497b1c250e3cb2e918982b25bb029c14603ac96f /theories/Compat
parent4b075af747f65bcd73ff1c78417cf77edf6fbd76 (diff)
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these.
Diffstat (limited to 'theories/Compat')
0 files changed, 0 insertions, 0 deletions