diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-27 16:29:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-27 16:59:29 +0100 |
| commit | b286c9f4f42febfd37f9715d81eaf118ab24aa94 (patch) | |
| tree | 77a696ea6d4de8d7b160f05c1c26c9aeff6448a7 /kernel/safe_typing.ml | |
| parent | 5f8c0bfbb04de58a527d373c3994592e5853d4e2 (diff) | |
Add support so that the type of a match in an inductive type with let-in
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. *)
Diffstat (limited to 'kernel/safe_typing.ml')
0 files changed, 0 insertions, 0 deletions