From dc078e3221f9781d0abd10c1432b0b9b443bdae7 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Mon, 23 Feb 2015 11:01:33 +0100
Subject: [PATCH] removed superfluous instances of try
---
lib/ModuRes/RA.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index bd3b8ed50..1d690ad32 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -358,9 +358,9 @@ Section Agreement.
destruct (eq_dec t0 t), (eq_dec t1 t0), (eq_dec t1 t); simpl; auto; try reflexivity;
rewrite e in e0; contradiction.
- destruct t1, t2; try reflexivity; compute; destruct (eq_dec t0 t), (eq_dec t t0);
- try reflexivity; auto; try contradiction; try (symmetry in e; contradiction).
+ try reflexivity; auto; try contradiction; symmetry in e; contradiction.
- destruct t; reflexivity.
- - destruct x, y; simpl; firstorder; try now inversion H.
+ - destruct x, y; simpl; firstorder; now inversion H.
- now constructor.
- destruct t1, t2; try contradiction; now constructor.
Qed.
--
GitLab