From c0553d59858b1e3e044cdc016b0b85f5bf2dd77b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 16 Sep 2007 19:09:23 +0000
Subject: Réponse à une incompatibilité introduite dans 10114 (calcul du nombre
 de solutions distinctes faites modulo égalité d'alias uniquement et pas
 modulo toute la puissance de la convertibilité)

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

(limited to 'test-suite/success')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ad69ced19e..26e62ae622 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -74,3 +74,15 @@ eauto.
 
 Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
 Check (exist _ O I : {n:nat|True}).
+
+(* An example (initially from Marseille/Fairisle) that involves an evar with
+   different solutions (Input, Output or bool) that may or may not be
+   considered distinct depending on which kind of conversion is used *)
+
+Section A.
+Definition STATE := (nat * bool)%type.
+Let Input := bool.
+Let Output := bool.
+Parameter Out : STATE -> Output.
+Check fun (s : STATE) (reg : Input) => reg = Out s.
+End A.
-- 
cgit v1.2.3