diff options
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 8 insertions, 0 deletions
@@ -6,6 +6,14 @@ Language - Slightly improved compilation of pattern-matching (slight source of incompatibilities) - Record's now accept anonymous fields "_" which does not build projections +- Changes in the allowed elimination sorts for certain class of +inductive definitions : + An inductive definition without constructors of Sort Prop can +be eliminated on sorts Set and Type + A "singleton" inductive definition (one constructor with arguments +in the sort Prop like conjunction of two propositions or equality) +can be eliminated directly on sort Type (In V7.2, only the sorts Prop and +Set were allowed) Tactics |