Add a test that rfstr can find a realDomainType in a tricky case

math-comp · Nov 24, 2022 · fa0ccff · fa0ccff
1 parent c9c4e35
commit fa0ccff
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/examples/lra_examples.v b/examples/lra_examples.v
@@ -109,6 +109,11 @@ Proof.
 lra.
 Qed.
 
+Lemma test_rfstr (x : rat) : (x <= 2%:R) || true = true.
+Proof.
+lra.
+Qed.
+
 End Tests.
 
 (* Examples from the test suite of Coq *)