diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-04-18 13:56:55 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-04-18 13:56:55 +0200 |
| commit | fd0fc9a8bd820d9ae1466a941a0a903efb8be7b6 (patch) | |
| tree | ec563bbd24b3e88b5df5423ca561d2f19a3b518d /Makefile.build | |
| parent | 1412f9f927d8bc412a2597c0ee09396bb9379d8b (diff) | |
Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)
Bug uncovered by ekcburak@hotmail.com
https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00006.html
Now, terms of the the form (Rinv t) are only syntaxified when t evaluates to a non-zero constant.
Diffstat (limited to 'Makefile.build')
0 files changed, 0 insertions, 0 deletions