diff options
| author | Pierre-Marie Pédrot | 2018-09-19 10:22:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-19 10:22:07 +0200 |
| commit | c32c8e2b18ea76087d9dbdb2b56a550aae61c917 (patch) | |
| tree | 605efaebda1c9f19fecc025ddc01f9e0bdb632a7 /test-suite/bugs | |
| parent | 44b8c4ec9acad33002b080ed0aefb214124db440 (diff) | |
| parent | c9c18edee8664e0e52ece7ef0ff83955f4eadcbd (diff) | |
Merge PR #7257: Fixing yet a source of dependency on alphabetic order in unification.
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/2670.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2670.v b/test-suite/bugs/closed/2670.v index c401420e94..791889b24b 100644 --- a/test-suite/bugs/closed/2670.v +++ b/test-suite/bugs/closed/2670.v @@ -15,6 +15,14 @@ Proof. refine (match e return _ with refl_equal => _ end). reflexivity. Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as a in _ = b return _ with refl_equal => _ end). + reflexivity. + Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as z in _ = y return _ with refl_equal => _ end). + reflexivity. + Undo 2. (* Next line similarly has a dependent and a non dependent solution *) refine (match e with refl_equal => _ end). reflexivity. |