diff options
| author | Matthieu Sozeau | 2014-10-08 17:25:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-10 20:40:04 +0200 |
| commit | 4dca32d9eabd2c5a1a239cfb8c3a33a0d962991c (patch) | |
| tree | 289abefff61c1966a091a12062efd62b9a0fab29 /kernel/inductive.ml | |
| parent | a806b1d47273b008507aa08a99e5e45fbfe5243b (diff) | |
Make constrMatching and detyping more robust with respect to
expand_projection failing if an innapropriate sigma is given.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions