aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3539.v
Commit message (Collapse)AuthorAge
* remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
|
* Removing option -no-native-compiler from test #3539 since this option is nowGravatar Hugo Herbelin2015-05-18
| | | | negated into -native-compiler.
* There are some occurs-check cases that can be handled by imitation (using ↵Gravatar Matthieu Sozeau2014-08-28
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).