From 616e576fd2e79e25464d61f4a9a78eabf5e2edef Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 15 Sep 2006 10:07:01 +0000
Subject: Report de l'heuristique d'unification premier ordre flexible/rigide
 en dernière étape de la procédure d'unification - Nouvelle fonction
 consider_remaining_unif_problems dédiée à la résolution   de l'unification
 premier ordre flexible/rigide - Déplacement check_evars dans Evarutil
 Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ?
 (cf exemples d'application dans test-suite/success/evars.v)

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

(limited to 'test-suite')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index baeec14781..ad69ced19e 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -68,3 +68,9 @@ Proof. trivial. Qed.
 Hint Resolve contradiction.
 Goal False.
 eauto.
+
+(* This used to fail in V8.1beta because first-order unification was
+   used before using type information *)
+
+Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
+Check (exist _ O I : {n:nat|True}).
-- 
cgit v1.2.3