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 /plugins/micromega/certificate.ml | |
| 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 'plugins/micromega/certificate.ml')
| -rw-r--r-- | plugins/micromega/certificate.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 914881db0..1561c811c 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -430,9 +430,6 @@ let nlinear_prover prfdepth (sys: (Mc.q Mc.pExpr * Mc.op1) list) = MonMap.fold (fun s m acc -> ((pol_of_mon m , Mc.NonStrict), Mc.PsatzSquare(norm0 (pol_of_mon s)))::acc) square [] in - Printf.printf "#square %i\n" (List.length square) ; - flush stdout ; - let sys = sys @ square in |