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 /theories/Sets/Powerset_Classical_facts.v | |
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 'theories/Sets/Powerset_Classical_facts.v')
0 files changed, 0 insertions, 0 deletions