diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-28 11:58:20 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-28 19:55:01 +0200 |
| commit | 3fdfb3ccb7986b1e4c7685b440a62730107a639f (patch) | |
| tree | e07a201af28e25a6513527b528d2c8b48b27af9d /lib/int.ml | |
| parent | ee6743d2879d874cad13bd05b5be3847ac27062e (diff) | |
There are some occurs-check cases that can be handled by imitation (using pruning),
hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but
backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
Diffstat (limited to 'lib/int.ml')
0 files changed, 0 insertions, 0 deletions