diff options
| author | herbelin | 2008-06-29 14:57:58 +0000 |
|---|---|---|
| committer | herbelin | 2008-06-29 14:57:58 +0000 |
| commit | 2040379ec1d79ff588498ca6f20d8c7b75d74533 (patch) | |
| tree | 030ab3eebf66961746ba164ca72a821a88d18851 /test-suite/success/evars.v | |
| parent | 42088723410c0aef9767ee0cd18735eb081f05a6 (diff) | |
Préférence donnée aux constantes qui ne sont pas des projections
canoniques lors d'une unification constante/constante s'apprêtant à
déplier l'une des deux constantes (suggestion des utilisateurs de
structures canoniques), ceci afin de préserver des possibilités
ultérieures de résolution d'evars par équipement en structure
canonique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11187 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/evars.v')
| -rw-r--r-- | test-suite/success/evars.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 082cbfbe17..3bc9c7f9e1 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -198,6 +198,11 @@ Goal forall x : nat, F1 x -> G1 x. refine (fun x H => proj2 (_ x H) _). Abort. +(* First-order unification between beta-redex (is it useful ?) *) + +Check fun (y: (forall x:((fun y:Type => bool) nat), True)) + (z: (fun z:Type => bool) _) => y z. + (* Remark: the following example does not succeed any longer in 8.2 because, the algorithm is more general and does exclude a solution that it should exclude for typing reason. Handling of types and backtracking is still to |