Commit f8248a86 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fixed opacity of Rcompare.

parent 3e062c4d
......@@ -410,7 +410,7 @@ unfold Rcompare.
now destruct (total_order_T x y) as [[H|H]|H] ; constructor.
Qed.
Opaque Rcompare.
Global Opaque Rcompare.
Theorem Rcompare_Lt :
forall x y,
......
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