diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-08 16:50:54 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-08 16:51:40 +0200 |
| commit | 2fceefe036f5f8289fd4667ade8b3240a11579d7 (patch) | |
| tree | 92ef9f4354b0f67189f913c5255443959cf135b3 /test-suite/success/AdvancedCanonicalStructure.v | |
| parent | 81c8acb84510de54424330ee83e4852e7610e27b (diff) | |
Fix canonical structure resolution in unification (bug found in Ssreflect).
Diffstat (limited to 'test-suite/success/AdvancedCanonicalStructure.v')
| -rw-r--r-- | test-suite/success/AdvancedCanonicalStructure.v | 28 |
1 files changed, 18 insertions, 10 deletions
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v index 97cf316ca..d819dc47a 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -47,6 +47,24 @@ Goal forall a1 a2, eqA (plusA a1 zeroA) a2. change (eqB (plusB (phi a1) zeroB) (phi a2)). Admitted. +Variable foo : A -> Type. + +Definition local0 := fun (a1 : A) (a2 : A) (a3 : A) => + (eq_refl : plusA a1 (plusA zeroA a2) = ia _). +Definition local1 := + fun (a1 : A) (a2 : A) (f : A -> A) => + (eq_refl : plusA a1 (plusA zeroA (f a2)) = ia _). + +Definition local2 := + fun (a1 : A) (f : A -> A) => + (eq_refl : (f a1) = ia _). + +Goal forall a1 a2, eqA (plusA a1 zeroA) a2. + intros a1 a2. + refine (eq_img _ _ _). +change (eqB (plusB (phi a1) zeroB) (phi a2)). +Admitted. + End group_morphism. Open Scope type_scope. @@ -129,13 +147,3 @@ Admitted. Check L : abs _ . End type_reification. - - - - - - - - - - |