| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin | |
| 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. *) | |||
| 2015-02-27 | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin | |
| clause in the presence of let-ins in the arity of inductive type). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |