From c975f79fd17181f4607a786e6f1444eef9fb5bb6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Dec 2001 08:57:20 +0000
Subject: 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
---
 test-suite/success/Case13.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 06149b3fa3..71c9191d63 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) 
-- 
cgit v1.2.3