From bf4fdaa1836a17e4d36d38ba47959d1f50155a7b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 29 May 2018 23:07:02 +0200
Subject: [ssr] under: rewrite takes an optional bool arg

* If this flag under=true: enable flag with_evars of refine_with
  to create evar(s) if the "under lemma" has non-inferable args.

* Backward compatibility of ssr rewrite is kept.

* Fix test-suite/ssr/dependent_type_err.v
---
 test-suite/prerequisite/ssr_mini_mathcomp.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index cb2c56736c..ca360f65a7 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -427,6 +427,8 @@ Lemma leqnSn n : n <= n.+1.             Proof. by elim: n. Qed.
 
 Lemma leq_trans n m p : m <= n -> n <= p -> m <= p.
 Admitted.
+Lemma leq_ltn_trans n m p : m <= n -> n < p -> m < p.
+Admitted.
 Lemma leqW m n : m <= n -> m <= n.+1.
 Admitted.
 Hint Resolve leqnSn.
-- 
cgit v1.2.3