Merge remote-tracking branch 'github/pr/339' into v8.6

Was PR#339: Documenting type class options, typeclasses eauto

4 files changed, 119 insertions, 18 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/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 8dadc2419c..efa4325264 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +46,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +109,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +121,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
new file mode 100644
index 0000000000..83d4ed69d4
--- /dev/null
+++ b/test-suite/bugs/closed/4095.v
@@ -0,0 +1,87 @@
+(* 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, then from 92 lines to 79 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Require Import TestSuite.admit.
+Require Import Coq.Setoids.Setoid.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+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.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end.
+  Undo.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
+    set(p:=P)
+  end. (* Toplevel input, characters 15-182:
+Error: Cannot infer an instance of type
+"PointedOPred" for the variable p in environment:
+T : Type
+O0 : T -> OPred
+O1 : T -> PointedOPred
+tr : T -> T
+O2 : PointedOPred
+x0 : T
+H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
index e884355fde..1e47f2957b 100644
--- a/test-suite/bugs/closed/4863.v
+++ b/test-suite/bugs/closed/4863.v
@@ -3,14 +3,14 @@ Require Import Classes.DecidableClass.
 Inductive Foo : Set :=
 | foo1 | foo2.
 
-Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
 Proof.
   intros P H.
   refine (Build_Decidable _ (if H then true else false) _).
   intuition congruence.
 Qed.
 
-Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances.
 
 Goal forall (a b : Foo), {a=b}+{a<>b}.
 intros.
@@ -21,7 +21,8 @@ Check ltac:(abstract (exact I)) : True.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.
-split. typeclasses eauto. typeclasses eauto. Qed.
+split. typeclasses eauto. 
+typeclasses eauto. Qed.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.