From 823f0ab9c34f99d9171a5332a535c20d9f0f315c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 30 Nov 2016 15:00:13 +0100 Subject: Fix typeclasses eauto shelving. A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl. --- test-suite/success/Typeclasses.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'test-suite') diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index f62427ef4..6b1f0315b 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -98,7 +98,7 @@ Goal exists R, @Refl nat R. solve [typeclasses eauto with foo]. Qed. -(* Set Typeclasses Compatibility "8.5". *) +Set Typeclasses Compatibility "8.5". Parameter f : nat -> Prop. Parameter g : nat -> nat -> Prop. Parameter h : nat -> nat -> nat -> Prop. @@ -108,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y. Hint Resolve a b c : mybase. Goal forall x y z, h x y z -> f x -> f y. intros. - Set Typeclasses Debug. - typeclasses eauto with mybase. + Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *) Unshelve. Abort. End bt. @@ -138,7 +137,8 @@ Notation "'return' t" := (unit t). Class A `(e: T) := { a := True }. Class B `(e_: T) := { e := e_; sg_ass :> A e }. -Set Typeclasses Debug. +(* Set Typeclasses Debug. *) +(* Set Typeclasses Debug Verbosity 2. *) Goal forall `{B T}, Prop. intros. apply a. -- cgit v1.2.3