diff options
| author | Matthieu Sozeau | 2014-06-19 12:43:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-19 12:44:52 +0200 |
| commit | 2a8e86e504e57d3c47d65fee408cec9aa9419445 (patch) | |
| tree | 7347d260cdbd398171c92abfa2b9125cacc852df /kernel/type_errors.ml | |
| parent | 83c17d79c3388ebd488559dcf99d5d019e60bb1c (diff) | |
- Fix bug in unification, not only named metas are turned into evars (e.g. in Ssreflect).
- Fix is_applied_rewrite_relation to look for propositional relations.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions