From d57e30cfe8f68987ed216415079f4dab42065408 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Nov 2015 17:26:36 +0100
Subject: Revert "Fixing #1225: we now skip the canonically built binding
 contexts of"

This reverts commit 07620386b3c1b535ee7e43306a6345f015a318f0.

Very sorry not ready.
---
 test-suite/bugs/closed/1225.v | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100644 test-suite/bugs/closed/1225.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/1225.v b/test-suite/bugs/closed/1225.v
deleted file mode 100644
index a7799b35fe..0000000000
--- a/test-suite/bugs/closed/1225.v
+++ /dev/null
@@ -1,12 +0,0 @@
-(* Taking automatically into account internal dependencies of a |match] *)
-
-Let a n := @exist nat _ _ (refl_equal (n + 1)).
-Goal let (n, _) := a 3 in n = 4.
-pattern 3 at 1.
-Abort.
-
-Goal match refl_equal 0 in _ = n return n = 0 with
-     | refl_equal => refl_equal 0
-     end = refl_equal 0.
-pattern 0 at 1 2 3 4 5 6.
-Abort.
-- 
cgit v1.2.3