diff options
| author | herbelin | 2011-11-21 11:41:29 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-21 11:41:29 +0000 |
| commit | 8cd666c100ae757b70d73f502878e4c939864ecc (patch) | |
| tree | 3005059684a4723a374eb91970d1fde7d3ec830e /kernel/type_errors.ml | |
| parent | 4ae1fb9619ce2505f0eb6b1f4a4eeed4d8e41489 (diff) | |
Add matching on non-inductive types in building an inversion problem
for finding the initial predicate, since their type can be dependent
on previous terms to match and they may have to be generalized.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14710 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions