From 20f9c0731990589b25878305bb793937962eca14 Mon Sep 17 00:00:00 2001
From: Thomas Braibant <thomas.braibant@inria.fr>
Date: Fri, 22 Mar 2013 14:30:19 +0100
Subject: [PATCH] WIP

---
 test.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/test.v b/test.v
index ba48336..a16fd94 100644
--- a/test.v
+++ b/test.v
@@ -80,7 +80,19 @@ Show Proof.
 Qed.  
 End sec_absu_2ismul3.
 
-
+Section vect. 
+  Variable A : Type. 
+  Inductive vector : nat -> Type :=
+    | nil : vector 0
+    | cons : forall n, A -> vector n -> vector (S n). 
+  
+  
+  Goal forall v : vector 0, v = nil. 
+  intros. 
+  Fail invert v. 
+  Abort. 
+End vect. 
+  
 
 Inductive tm : Type :=
   | const : nat -> tm