Commit 6573e072 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add missing inequality reification.

parent 4d8192b2
......@@ -88,6 +88,8 @@ Ltac massage_goal :=
| |- (Rabs ?x <= ?v)%R => aux v x (Gabsle true)
| |- (?u <= ?x)%R => aux u x (Gge true)
| |- (?x <= ?v)%R => aux v x (Gle true)
| |- (?x >= ?u)%R => aux u x (Gge false)
| |- (?v >= ?x)%R => aux v x (Gle false)
| |- (?u <= ?x <= ?v)%R =>
let u := reify u (@nil R) in
aux v x (Glele u)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment