Fix handling of only_classes at toplevel

3 files changed, 148 insertions, 48 deletions

diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index fcdfa0057b..ff515038ec 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -1,4 +1,3 @@
-Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
 Require Coq.Setoids.Setoid.
 Import Coq.Setoids.Setoid.
@@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops.
 Local Existing Instance ILFun_ILogic.
 Definition catOP (P Q: OPred) : OPred := admit.
 Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
-admit.
+apply admit.
 Defined.
 Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
 Class IsPointed (T : Type) := point : T.
@@ -69,8 +68,26 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     pose P;
     refine (P _ _)
   end; unfold Basics.flip.
-  2: solve [ apply reflexivity ].
-  Undo.
-  2: reflexivity. (* Toplevel input, characters 18-29:
-Error:
-Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
+  Focus 2.
+  Set Typeclasses Debug.
+  Set Typeclasses Legacy Resolution.
+  apply reflexivity.
+  (* Debug: 1.1: apply @IsPointed_catOP on
+(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0))
+Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0))
+Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x))
+Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails)
+Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities
+Debug: Backtracking after apply @Equivalence_Reflexive
+Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails)
+Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails)
+Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
+*)
+  Undo. Unset Typeclasses Legacy Resolution.
+  Test Typeclasses Unique Solutions.
+  Test Typeclasses Unique Instances.
+  Show Existentials.
+  Set Typeclasses Debug Verbosity 2.
+  Set Printing All.
+  Fail apply reflexivity.
+  
\ No newline at end of file
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 651bbf7d28..4581a7ce40 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -5,12 +5,40 @@ Module onlyclasses.
   Hint Extern 0 Foo => exact foo : typeclass_instances.
   Goal Foo * Foo.
     split. shelve.
-    Fail typeclasses eauto.
+    Set Typeclasses Debug.
+    typeclasses eauto.
     typeclasses eauto with typeclass_instances.
     Unshelve. typeclasses eauto with typeclass_instances.
   Abort.
 End onlyclasses.
 
+Module shelve_non_class_subgoals.
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Class Bar := {}.
+  Instance bar1 (f:Foo) : Bar.
+
+  Typeclasses eauto := debug.
+  Set Typeclasses Debug Verbosity 2.
+  Goal Bar.
+    (* Solution has shelved subgoals *)
+    Fail typeclasses eauto.
+  Abort.
+End shelve_non_class_subgoals.
+
+Module shelve_non_class_subgoals2.
+  Class Bar := {}.
+
+  Instance bar1 (t:Type) : Bar.
+  Hint Extern 0 => exact True : typeclass_instances.
+  Typeclasses eauto := debug.
+  Goal Bar.
+    Fail typeclasses eauto.
+    debug eauto with typeclass_instances.
+  Qed.  
+End shelve_non_class_subgoals2.
+
 Module bt.
 Require Import Equivalence.
 
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 4db547f4e4..9bcecfe1f3 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -5,7 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Require Import List.
 
 Class A (A : Type).
   Instance an: A nat.
@@ -31,6 +30,8 @@ Defined.
 
 Hint Extern 0 (_ /\ _) => constructor : typeclass_instances.
 
+Existing Class and.
+
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
   eexists. eexists. typeclasses eauto.
@@ -46,7 +47,7 @@ Class C {T} `(a : A T) (t : T).
 Require Import Classes.Init.
 Hint Extern 0 { x : ?A & _ } =>
   unshelve class_apply @existT : typeclass_instances.
-
+Existing Class sigT.
 Set Typeclasses Debug.
 Instance can: C an 0.
 (* Backtrack on instance implementation *)
@@ -63,41 +64,6 @@ Proof.
 Defined.
   
 
-Parameter in_list : list (nat * nat) -> nat -> Prop.
-Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
-  ~ in_list l n.
-
-(* Hints Unfold not_in_list. *)
-
-Axiom
-  lem1 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
-
-Axiom
-  lem2 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
-
-Axiom
-  lem3 :
-    forall (l : list (nat * nat)) (n p q : nat),
-    not_in_list ((p, q) :: l) n -> not_in_list l n.
-
-Axiom
-  lem4 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
-
-Hint Resolve lem1 lem2 lem3 lem4: essai.
-
-Goal
-forall (l : list (nat * nat)) (n p q : nat),
-not_in_list ((p, q) :: l) n -> not_in_list l n.
-  intros.
-  eauto with essai.
-Qed.
-
 (* Example from Nicolas Magaud on coq-club - Jul 2000 *)
 
 Definition Nat : Set := nat.
@@ -126,6 +92,9 @@ Qed.
   Full backtracking on dependent subgoals.
  *)
 Require Import Coq.Classes.Init.
+
+Module NTabareau.
+
 Set Typeclasses Dependency Order.
 Unset Typeclasses Iterative Deepening.
 Notation "x .1" := (projT1 x) (at level 3).
@@ -149,7 +118,8 @@ Hint Extern 5 (Bar ?D.1) =>
 Hint Extern 5 (Qux ?D.1) =>
     destruct D; simpl : typeclass_instances.
 
-Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances.
+Hint Extern 1 myType =>
+  unshelve refine (fooTobar _ _).1 : typeclass_instances.
 
 Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
 
@@ -158,8 +128,93 @@ Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instance
 Unset Typeclasses Debug.
 Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
 Proof.
-  Time typeclasses eauto 10.
+  Time typeclasses eauto 10 with typeclass_instances.
   Undo. Set Typeclasses Iterative Deepening.
-  Time typeclasses eauto.
+  Time typeclasses eauto with typeclass_instances.
 Defined.
 
+End NTabareau.
+
+Module NTabareauClasses.
+
+Set Typeclasses Dependency Order.
+Unset Typeclasses Iterative Deepening.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+
+Parameter myType: Type. 
+Existing Class myType.
+
+Class Foo (a:myType) := {}.
+
+Class Bar (a:myType) := {}.
+
+Class Qux (a:myType) := {}.
+
+Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.
+
+Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}.
+
+Hint Extern 5 (Bar ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 5 (Qux ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances.
+
+Hint Extern 0 { x : _ & _ } =>
+  unshelve notypeclasses refine (existT _ _ _) : typeclass_instances.
+
+Unset Typeclasses Debug.
+
+Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
+Proof.
+  Time typeclasses eauto 10 with typeclass_instances.
+  Undo. Set Typeclasses Iterative Deepening.
+  Time typeclasses eauto with typeclass_instances.
+Defined.
+
+End NTabareauClasses.
+
+
+Require Import List.
+
+Parameter in_list : list (nat * nat) -> nat -> Prop.
+Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
+  ~ in_list l n.
+
+(* Hints Unfold not_in_list. *)
+
+Axiom
+  lem1 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
+
+Axiom
+  lem2 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
+
+Axiom
+  lem3 :
+    forall (l : list (nat * nat)) (n p q : nat),
+    not_in_list ((p, q) :: l) n -> not_in_list l n.
+
+Axiom
+  lem4 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
+
+Hint Resolve lem1 lem2 lem3 lem4: essai.
+
+Goal
+forall (l : list (nat * nat)) (n p q : nat),
+not_in_list ((p, q) :: l) n -> not_in_list l n.
+  intros.
+  eauto with essai.
+Qed.