diff options
author | 2016-10-12 11:22:53 +0200 | |
---|---|---|
committer | 2016-10-12 11:22:53 +0200 | |
commit | 6e49be2c03f11f412d17e41ca2e74232d12d915c (patch) | |
tree | e8a55b1349d84ba35856b5fd764ed4023a7f1d95 /test-suite/bugs/closed | |
parent | 6d55121c90ec50319a3de6a6907726fbcdc2f835 (diff) | |
parent | 2bcae5b7a22019718973f65cafd271f735d3d85b (diff) |
Merge remote-tracking branch 'git/bug5123' into v8.5
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/5123.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v new file mode 100644 index 000000000..bcde510ee --- /dev/null +++ b/test-suite/bugs/closed/5123.v @@ -0,0 +1,33 @@ +(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *) + +(*Pose an open constr to prevent immediate typeclass resolution in holes:*) +Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H. + +Inductive vect A : nat -> Type := +| vnil : vect A 0 +| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n). + +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Require Bool. + +Instance Bool_eqdec : Eqdec bool := Bool.bool_dec. + +Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}. + +Typeclasses eauto := debug. + +Goal True. + unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. + all:cycle 2. + eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. +Abort. + +Goal True. + opose (@vect_sigT_eqdec _ _ _ _) as H. + Unshelve. + all:cycle 3. + eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. +Abort.
\ No newline at end of file |