From 2630d3b139386f05396940a3d8664b92f37758f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 7 Nov 2019 01:16:05 +0100
Subject: [PATCH] do not rely on vlib 'des' tactic
---
util/bigcat.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/util/bigcat.v b/util/bigcat.v
index c99779f71..8fd7ebee5 100644
--- a/util/bigcat.v
+++ b/util/bigcat.v
@@ -10,7 +10,7 @@ Section BigCatLemmas.
x \in (f j) ->
x \in \cat_(m <= i < n) (f i).
Proof.
- intros T x m n j f LE IN; move: LE => /andP LE; des.
+ intros T x m n j f LE IN; move: LE => /andP [LE LE0].
rewrite -> big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
rewrite mem_cat; apply/orP; right.
destruct n; first by rewrite ltn0 in LE0.
@@ -30,7 +30,7 @@ Section BigCatLemmas.
rewrite big_nat_recr // /= mem_cat in IN.
move: IN => /orP [HEAD | TAIL].
{
- apply IHn in HEAD; destruct HEAD; exists x0; des.
+ apply IHn in HEAD; destruct HEAD; exists x0. move: H => [H /andP [H0 H1]].
split; first by done.
by apply/andP; split; [by done | by apply ltnW].
}
@@ -157,4 +157,4 @@ Section BigCatLemmas.
by apply leq_sum; ins; apply SIZE.
Qed.
-End BigCatLemmas.
\ No newline at end of file
+End BigCatLemmas.
--
GitLab