diff options
| author | herbelin | 2011-12-04 20:48:32 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-04 20:48:32 +0000 |
| commit | 095eee7e2ae4a1715683e766af973c28500583f0 (patch) | |
| tree | 1e053216380517db302e1ace1b7265887ccc5a7e /kernel/type_errors.mli | |
| parent | e47cdbd232517adf6e6bf411b9f9715c43773fd5 (diff) | |
Fixed a small regression in pattern-matching compilation introduced in
r14737 (when to expand an alias). However, the heuristic remains
different as before r14737 since we stopped taking into account the
dependency in the predicate to take the decision of expanding or not.
Let's see if we can eventually fine-tuning this.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14760 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions