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

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ad69ced19..26e62ae62 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.