Merge branch 'ordtype' into Coq-8.5

math-comp · May 6, 2016 · 4d6839f · 4d6839f
2 parents 7f0ccd6 + 763315c
commit 4d6839f
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/theories/Basic/ordtype.v b/theories/Basic/ordtype.v
@@ -137,7 +137,7 @@ Lemma gtnX_eqF m n : m < n -> n == m = false.
 Proof. rewrite [(n == m)]eq_sym. exact: ltnX_eqF. Qed.
 
 Lemma leqX_eqVltnX m n : (m <= n) = (m == n) || (m < n).
-Proof. rewrite /ltnX_op; by case eqP => [/= -> | /= _]; first by rewrite (leqXnn n). Qed.
+Proof. rewrite /ltnX_op; by case eqP => [/= -> | /= _]; first by rewrite leqXnn. Qed.
 
 Lemma ltnX_neqAleqX m n : (m < n) = (m != n) && (m <= n).
 Proof. by []. Qed.
@@ -1204,7 +1204,7 @@ Variable T : pordType.
 Fact geqX_order : PartOrder.axiom (@geqX T).
 Proof.
   split.
-  - move=> n /=; by apply: leqXnn.
+  - by move=> n /=.
   - move=> m n /= /andP [] H1 H2; apply/eqP; by rewrite eqn_leqX H1 H2.
   - move=> m n p /= H1 H2; by apply: (leqX_trans H2 H1).
 Qed.

diff --git a/theories/LRrule/Schensted.v b/theories/LRrule/Schensted.v
@@ -240,7 +240,7 @@ Section Insert.
   Lemma ins_leq i : i < size Row -> (nth l ins i <= nth l Row i)%Ord.
   Proof.
     rewrite -insE /insmin nth_set_nth /=.
-    case eqP => [->|_ _]; last exact: leqXnn.
+    case eqP => [->|_ _ //].
     rewrite /mininspred /inspred; case (ltnXP l (last l Row)) => [Hcase | Hcase].
     - set exP := ex_intro _ _ _; case (ex_minnP exP) => pos Hl _ _; exact: ltnXW.
     - by rewrite ltnn.
@@ -369,7 +369,7 @@ Section Schensted.
           apply: (is_rowP _ _ HSch).
           have:= Hsz; rewrite -{1}(ltn_predK Hsz) ltnS => -> /=.
           rewrite -{2}(ltn_predK Hsz); exact: ltnSn.
-        + case eqP => [_ | Habs]; first exact: leqXnn.
+        + case eqP => [// | Habs].
           exfalso; rewrite ltnS in Hsz; move: Habs => /eqP; by rewrite eqn_leq Hsz Hszlt.
 
     (* The subsequence doesn't end by wn *)