| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add support so that the type of a match in an inductive type with let-in |  Hugo Herbelin | 2015-02-27 |
| | | | | | | | | | | is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *) | ||
| * | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin | 2015-02-27 |
| clause in the presence of let-ins in the arity of inductive type). | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |