From 56b8bf5bdada4a09ace234c96304b4898def9664 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Sep 2006 08:34:51 +0000
Subject: Ajout unification pattern dans l'algorithme d'unification des
 tactiques (unification.ml) + renommages (evarconv.ml) + exemple
 (unification.v)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9131 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/unification.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 60c03831a0..6886962156 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -48,3 +48,18 @@ Parameter t: L (unit + unit).
 Check (f (fun x : unit + unit =>
   sum_rec (fun _ : unit + unit => L unit)
     (fun y => c y) (fun y => c y) x) t).
+
+
+(* Test patterns unification in apply *)
+
+Require Import Arith.
+Parameter x y : nat.
+Parameter G:x=y->x=y->Prop.
+Parameter K:x<>y->x<>y->Prop.
+Lemma l3 : (forall f:x=y->Prop, forall g:x<>y->Prop,
+            match eq_nat_dec x y with left a => f a | right a => g a end)
+   -> match eq_nat_dec x y with left a => G a a | right a => K a a end.
+Proof.
+intros.
+apply H.
+Qed.
-- 
cgit v1.2.3