Un peu plus d'inférence des ? traitée par le Cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2323 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 5 deletions

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 06149b3fa..71c9191d6 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -12,16 +12,13 @@ Check [x]Cases x of (C2 n) => O | O => O | (S n) => n end.
 (* Coercion not at the root of pattern *)
 Check [x]Cases x of (C2 O) => O | _ => O end.
 
-(* TODO: insert unification inside patterns to get these examples working
-
+(* Unification and coercions inside patterns *)
 Check [x:(option nat)]Cases x of None => O | (Some O) => O | _ => O end.
 
-(* Coercion up to delta-conversion *)
+(* Coercion up to delta-conversion, and unification *)
 Coercion somenat := (Some nat).
 Check [x]Cases x of None => O | O => O | (S n) => n end.
 
-*)
-
 (* Coercions with parameters *)
 Inductive listn : nat-> Set := 
   niln : (listn O)