From be11ab322fa73804118738e7a08e9910fdf4600d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Oct 2016 11:03:13 +0200
Subject: Renamings to avoid confusion deprecating old names

reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
---
 tactics/class_tactics.ml | 2 +-
 tactics/equality.ml      | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0944cbe38f..9ea4027263 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1437,7 +1437,7 @@ let initial_select_evars filter =
 
 let resolve_typeclass_evars debug depth unique env evd filter split fail =
   let evd =
-    try Evarconv.consider_remaining_unif_problems
+    try Evarconv.solve_unif_constraints_with_heuristics
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
     with e when CErrors.noncritical e -> evd
   in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e9d08d7375..bb3cbad92b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1163,7 +1163,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
 	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
-	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
+	let () =
+          evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
 	error "Cannot solve a unification problem."
-- 
cgit v1.2.3


From 13738c4afd217ea7d71e654c38fc6a661bd2953c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 24 Oct 2016 13:38:07 +0200
Subject: Fix printing of typeclasses eauto debug wrt intro.

---
 tactics/class_tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0944cbe38f..248635b4e4 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1141,7 +1141,8 @@ module Search = struct
                        (true,false,false) info.search_only_classes None decl in
     let ldb = Hint_db.add_list env s hint info.search_hints in
     let info' =
-      { info with search_hints = ldb; last_tac = lazy (str"intro") }
+      { info with search_hints = ldb; last_tac = lazy (str"intro");
+        search_depth = 1 :: 1 :: info.search_depth }
     in kont info'
 
   let intro info kont =
-- 
cgit v1.2.3


From 2d687dec5709695942aa6a92197a5e5e2a91b616 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 24 Oct 2016 17:35:04 +0200
Subject: Remove v62 from the codebase.

---
 tactics/auto.mli | 8 +++-----
 tactics/eauto.ml | 4 +---
 tactics/hints.ml | 3 +--
 3 files changed, 5 insertions(+), 10 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 5384140c2a..04791a526e 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -48,17 +48,15 @@ val new_auto : ?debug:Tacexpr.debug ->
 (** auto with default search depth and with the hint database "core" *)
 val default_auto : unit Proofview.tactic
 
-(** auto with all hint databases except the "v62" compatibility database *)
+(** auto with all hint databases *)
 val full_auto : ?debug:Tacexpr.debug ->
   int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
 
-(** auto with all hint databases except the "v62" compatibility database
-   and doing delta *)
+(** auto with all hint databases and doing delta *)
 val new_full_auto : ?debug:Tacexpr.debug ->
   int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
 
-(** auto with default search depth and with all hint databases
-   except the "v62" compatibility database *)
+(** auto with default search depth and with all hint databases *)
 val default_full_auto : unit Proofview.tactic
 
 (** The generic form of auto (second arg [None] means all bases) *)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index c6d2448679..480185337b 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -410,9 +410,7 @@ let eauto ?(debug=Off) np lems dbnames =
   tclTRY (e_search_auto debug np lems db_list)
 
 let full_eauto ?(debug=Off) n lems gl =
-  let dbnames = current_db_names () in
-  let dbnames =  String.Set.remove "v62" dbnames in
-  let db_list = List.map searchtable_map (String.Set.elements dbnames) in
+  let db_list = current_pure_db () in
   tclTRY (e_search_auto debug n lems db_list) gl
 
 let gen_eauto ?(debug=Off) np lems = function
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 89ecc6c0b2..1ebd32c378 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -657,8 +657,7 @@ let searchtable_add (name,db) =
 let current_db_names () = Hintdbmap.domain !searchtable
 let current_db () = Hintdbmap.bindings !searchtable
 
-let current_pure_db () =
-  List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
+let current_pure_db () = List.map snd (current_db ())
 
 let error_no_such_hint_database x =
   errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
-- 
cgit v1.2.3


From e807f3407fb19f481dac332e7650eddfa9b5fd5d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 14 Oct 2016 16:53:19 +0200
Subject: Documenting changes in typeclasses

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d2e5d8525d..88e84f4183 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -83,7 +83,7 @@ let _ =
 
 let apply_solve_class_goals = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optsync = true; Goptions.optdepr = true;
   Goptions.optname =
     "Perform typeclass resolution on apply-generated subgoals.";
   Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"];
-- 
cgit v1.2.3


From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 24 Oct 2016 18:18:33 +0200
Subject: Lets Hints/Instances take an optional pattern

In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
---
 tactics/class_tactics.ml | 18 ++++++----
 tactics/hints.ml         | 87 +++++++++++++++++++++++++-----------------------
 tactics/hints.mli        | 36 ++++++++++++++------
 3 files changed, 83 insertions(+), 58 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9cb6b7fe78..da91674f5d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -539,10 +539,16 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
       let name = PathHints [VarRef id] in
       let hints =
         if is_class then
-          let hints = build_subclasses ~check:false env sigma (VarRef id) None in
+          let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
             (List.map_append
-               (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
-                  (true,false,Flags.is_verbose()) pri false
+             (fun (path,info,c) ->
+	      let info =
+		{ info with Vernacexpr.hint_pattern =
+			    Option.map (Constrintern.intern_constr_pattern env)
+				       info.Vernacexpr.hint_pattern }
+	      in
+	      make_resolves env sigma ~name:(PathHints path)
+                  (true,false,Flags.is_verbose()) info false
                  (IsConstr (c,Univ.ContextSet.empty)))
                hints)
         else []
@@ -567,7 +573,7 @@ let make_hints g st only_classes sign =
         in
         if consider then
           let hint =
-            pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+            pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp
           in hint @ hints
         else hints)
       ([]) sign
@@ -636,7 +642,7 @@ module V85 = struct
             let env = Goal.V82.env s g' in
             let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
             let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
-              (true,false,false) info.only_classes None (List.hd context) in
+              (true,false,false) info.only_classes empty_hint_info (List.hd context) in
             let ldb = Hint_db.add_list env s hint info.hints in
             (g', { info with is_evar = None; hints = ldb;
                              auto_last_tac = lazy (str"intro") })) gls
@@ -1140,7 +1146,7 @@ module Search = struct
     let decl = Tacmach.New.pf_last_hyp gl in
     let hint =
       make_resolve_hyp env s (Hint_db.transparent_state info.search_hints)
-                       (true,false,false) info.search_only_classes None decl in
+                       (true,false,false) info.search_only_classes empty_hint_info decl in
     let ldb = Hint_db.add_list env s hint info.search_hints in
     let info' =
       { info with search_hints = ldb; last_tac = lazy (str"intro") }
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 823af0b0a5..9cbfe20d96 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -84,6 +84,8 @@ let secvars_of_hyps hyps =
   if all then Id.Pred.full (* If the whole section context is available *)
   else pred
 
+let empty_hint_info = Vernacexpr.{ hint_priority = None; hint_pattern = None }
+
 (************************************************************************)
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
@@ -736,7 +738,7 @@ let secvars_of_constr env c =
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global_reference env gr)
 
-let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env c in
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
@@ -747,16 +749,17 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
 	in
-          (Some hd,
-	  { pri = (match pri with None -> 0 | Some p -> p);
-	    poly = poly;
-	    pat = Some pat;
-	    name = name;
-            db = None;
-            secvars;
-	    code = with_uid (Give_exact (c, cty, ctx)); })
+	let pri = match info.hint_priority with None -> 0 | Some p -> p in
+	let pat = match info.hint_pattern with
+	| Some pat -> snd pat
+	| None -> pat
+	in
+        (Some hd,
+	 { pri; poly; pat = Some pat; name;
+	   db = None; secvars;
+	   code = with_uid (Give_exact (c, cty, ctx)); })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
     match kind_of_term cty with
     | Prod _ ->
@@ -769,12 +772,13 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
           with BoundPattern -> failwith "make_apply_entry" in
         let nmiss = List.length (clenv_missing ce) in
         let secvars = secvars_of_constr env c in
+	let pri = match info.hint_priority with None -> nb_hyp cty + nmiss | Some p -> p in
+	let pat = match info.hint_pattern with
+	| Some p -> snd p | None -> pat
+	in
 	if Int.equal nmiss 0 then
 	  (Some hd,
-          { pri = (match pri with None -> nb_hyp cty | Some p -> p);
-	    poly = poly;
-            pat = Some pat;
-	    name = name;
+          { pri; poly; pat = Some pat; name;
             db = None;
             secvars;
             code = with_uid (Res_pf(c,cty,ctx)); })
@@ -784,12 +788,8 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++
 	    str " will only be used by eauto");
           (Some hd,
-           { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
-	     poly = poly;
-             pat = Some pat;
-	     name = name;
-             db = None;
-             secvars;
+           { pri; poly; pat = Some pat; name;
+	     db = None; secvars;
              code = with_uid (ERes_pf(c,cty,ctx)); })
         end
     | _ -> failwith "make_apply_entry"
@@ -840,14 +840,14 @@ let fresh_global_or_constr env sigma poly cr =
       (c, Univ.ContextSet.empty)
     end
 
-let make_resolves env sigma flags pri poly ?name cr =
+let make_resolves env sigma flags info poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-                             [make_exact_entry env sigma pri poly ?name;
-                              make_apply_entry env sigma flags pri poly ?name]
+			     [make_exact_entry env sigma info poly ?name;
+			      make_apply_entry env sigma flags info poly ?name]
   in
   if List.is_empty ents then
     errorlabstrm "Hint"
@@ -861,7 +861,7 @@ let make_resolve_hyp env sigma decl =
   let hname = get_id decl in
   let c = mkVar hname in
   try
-    [make_apply_entry env sigma (true, true, false) None false
+    [make_apply_entry env sigma (true, true, false) empty_hint_info false
        ~name:(PathHints [VarRef hname])
        (c, get_type decl, Univ.ContextSet.empty)]
   with
@@ -1145,16 +1145,17 @@ let add_transparency l b local dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_extern pri pat tacast local dbname =
-  let pat = match pat with
+let add_extern info tacast local dbname =
+  let pat = match info.hint_pattern with
   | None -> None
   | Some (_, pat) -> Some pat
   in
-  let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in
+  let hint = make_hint ~local dbname
+		       (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
   Lib.add_anonymous_leaf (inAutoHint hint)
 
-let add_externs pri pat tacast local dbnames =
-  List.iter (add_extern pri pat tacast local) dbnames
+let add_externs info tacast local dbnames =
+  List.iter (add_extern info tacast local) dbnames
 
 let add_trivials env sigma l local dbnames =
   List.iter
@@ -1168,15 +1169,16 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make ()
 
 type hnf = bool
 
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
 type hints_entry =
-  | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list
+  | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
   | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
-  | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * glob_tactic_expr
+  | HintsExternEntry of hint_info * glob_tactic_expr
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -1240,11 +1242,12 @@ let interp_hints poly =
 	(PathHints [gr], poly, IsGlobRef gr)
     | HintsConstr c -> (PathAny, poly, f poly c)
   in
-  let fres (pri, b, r) =
+  let fp = Constrintern.intern_constr_pattern (Global.env()) in
+  let fres (info, b, r) =
     let path, poly, gr = fi r in
-      (pri, poly, b, path, gr)
+    let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
+      (info, poly, b, path, gr)
   in
-  let fp = Constrintern.intern_constr_pattern (Global.env()) in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
   | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
@@ -1260,14 +1263,14 @@ let interp_hints poly =
           List.init (nconstructors ind) 
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
-			None, mib.Declarations.mind_polymorphic, true, 
+			empty_hint_info, mib.Declarations.mind_polymorphic, true,
 			PathHints [gr], IsGlobRef gr)
       in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
       let pat =	Option.map fp patcom in
       let l = match pat with None -> [] | Some (l, _) -> l in
       let tacexp = Hook.get forward_intern_tac l tacexp in
-      HintsExternEntry (pri, pat, tacexp)
+      HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
 let add_hints local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
@@ -1283,8 +1286,8 @@ let add_hints local dbnames0 h =
   | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
   | HintsTransparencyEntry (lhints, b) ->
       add_transparency lhints b local dbnames
-  | HintsExternEntry (pri, pat, tacexp) ->
-      add_externs pri pat tacexp local dbnames
+  | HintsExternEntry (info, tacexp) ->
+      add_externs info tacexp local dbnames
 
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
@@ -1308,7 +1311,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
   let lems = expand_constructor_hints env sigma lems in
   let hintlist' =
     List.map_append (fun (poly, lem) ->
-		     make_resolves env sigma (eapply,true,false) None poly lem) lems in
+		     make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in
   Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
@@ -1362,7 +1365,9 @@ let pr_hint h = match h.obj with
       (str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
 
 let pr_id_hint (id, v) =
-  (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+  let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in
+  (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
+   ++ str", id " ++ int id ++ str ")" ++ spc ())
 
 let pr_hint_list hintlist =
   (str "  " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 8145ae1936..42a2896ed8 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -27,6 +27,8 @@ val decompose_app_bound : constr -> global_reference * constr array
 
 val secvars_of_hyps : Context.Named.t -> Id.Pred.t
 
+val empty_hint_info : 'a hint_info_gen
+
 (** Pre-created hint databases *)
 
 type 'a hint_ast =
@@ -129,20 +131,21 @@ type hint_db = Hint_db.t
 
 type hnf = bool
 
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
 type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
 type hints_entry =
-  | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * 
-			  hint_term) list
+  | HintsResolveEntry of
+    (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
   | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
-  | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+  | HintsExternEntry of hint_info * Tacexpr.glob_tactic_expr
 
 val searchtable_map : hint_db_name -> hint_db
 
@@ -169,23 +172,34 @@ val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
   env -> evar_map -> open_constr -> hint_term
 
-(** [make_exact_entry pri (c, ctyp, ctx, secvars)].
+(** [make_exact_entry info (c, ctyp, ctx)].
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c].
-   [ctx] is its (refreshable) universe context. *)
-val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom -> 
+   [ctx] is its (refreshable) universe context. 
+   In info:
+   [hint_priority] is the hint's desired priority, it is 0 if unspecified
+   [hint_pattern] is the hint's desired pattern, it is inferred if not specified
+*)
+
+val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   (constr * types * Univ.universe_context_set) -> hint_entry
 
-(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty,ctx,secvars)].
+(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
    [eapply] is true if this hint will be used only with EApply;
    [hnf] should be true if we should expand the head of cty before searching for
    products;
    [c] is the term given as an exact proof to solve the goal;
    [cty] is the type of [c].
-   [ctx] is its (refreshable) universe context. *)
+   [ctx] is its (refreshable) universe context. 
+   In info:
+   [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty]
+   if unspecified
+   [hint_pattern] is the hint's desired pattern, it is inferred from the conclusion of [cty]
+   if not specified
+*)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> 
+  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   (constr * types * Univ.universe_context_set) -> hint_entry
 
 (** A constr which is Hint'ed will be:
@@ -196,7 +210,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> 
+  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
-- 
cgit v1.2.3


From b57c7005d81b35b2ae6c45e6ac3088a73b3c43b2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Oct 2016 18:31:03 +0200
Subject: Fix Typeclasses eauto := bfs.

---
 tactics/class_tactics.ml  | 6 ++++++
 tactics/class_tactics.mli | 4 ++++
 2 files changed, 10 insertions(+)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index da91674f5d..c1ba645beb 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -181,6 +181,12 @@ let set_typeclasses_depth =
       optread  = get_typeclasses_depth;
       optwrite = set_typeclasses_depth; }
 
+type search_strategy = Dfs | Bfs
+
+let set_typeclasses_strategy = function
+  | Dfs -> set_typeclasses_iterative_deepening true
+  | Bfs -> set_typeclasses_iterative_deepening false
+
 let pr_ev evs ev =
   Printer.pr_constr_env (Goal.V82.env evs ev) evs
                         (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 8db264ad95..565415a95e 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -20,6 +20,10 @@ val get_typeclasses_debug : unit -> bool
 val set_typeclasses_depth : int option -> unit
 val get_typeclasses_depth : unit -> int option
 
+type search_strategy = Dfs | Bfs
+
+val set_typeclasses_strategy : search_strategy -> unit
+
 val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
                         depth:(Int.t option) ->
                         Hints.hint_db_name list -> unit Proofview.tactic
-- 
cgit v1.2.3


From ced1e16d43bd896b7e8473921a29749a0ba35643 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Oct 2016 18:31:46 +0200
Subject: Fix bugs in Filtered Unification and cleanup code

---
 tactics/class_tactics.ml | 58 ++++++++++++++++++++++++++++++------------------
 1 file changed, 36 insertions(+), 22 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c1ba645beb..264df52154 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -246,12 +246,11 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   end }
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine poly flags =
+let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
   let open Clenv in
-  { enter = begin fun gls ((c, t, ctx),n,clenv) ->
-    let env = Proofview.Goal.env gls in
-    let concl = Proofview.Goal.concl gls in
-    Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
+  let env = Proofview.Goal.env gls in
+  let concl = Proofview.Goal.concl gls in
+  Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
       let sigma = Sigma.to_evar_map sigma in
       let sigma, term, ty =
         if poly then
@@ -266,15 +265,20 @@ let unify_resolve_refine poly flags =
       let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
       let term = applistc term (List.map (fun x -> x.hole_evar) cl.cl_holes) in
       let sigma' =
-        let evdref = ref sigma' in
-        if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
-                                      evdref cl.cl_concl concl) then
-          Type_errors.error_actual_type env
-            {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
-            concl;
-        !evdref
+        Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta
+                                cl.cl_concl concl sigma'
       in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
-  end }
+
+let unify_resolve_refine poly flags gl clenv =
+  Proofview.tclORELSE
+    (unify_resolve_refine poly flags gl clenv)
+    (fun ie ->
+      match fst ie with
+      | Evarconv.UnableToUnify _ ->
+         Tacticals.New.tclZEROMSG (str "Unable to unify")
+      | e when CErrors.noncritical e ->
+         Tacticals.New.tclZEROMSG (str "Unexpected error")
+      | _ -> iraise ie)
 
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
@@ -295,9 +299,11 @@ let clenv_of_prods poly nprods (c, clenv) gl =
 let with_prods nprods poly (c, clenv) f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.nf_enter { enter = begin fun gl ->
-     match clenv_of_prods poly nprods (c, clenv) gl with
-     | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
-     | Some (diff, clenv') -> f.enter gl (c, diff, clenv') end }
+      try match clenv_of_prods poly nprods (c, clenv) gl with
+          | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+          | Some (diff, clenv') -> f.enter gl (c, diff, clenv')
+      with e when CErrors.noncritical e ->
+        Tacticals.New.tclFAIL 0 (CErrors.print e) end }
   else Proofview.Goal.nf_enter
          { enter = begin fun gl ->
                    if Int.equal nprods 0 then f.enter gl (c, None, clenv)
@@ -312,7 +318,7 @@ let matches_pattern concl pat =
        if Constr_matching.is_matching env sigma pat concl then
          Proofview.tclUNIT ()
        else
-         Tacticals.New.tclZEROMSG (str "conclPattern")
+         Tacticals.New.tclZEROMSG (str "pattern does not match")
   in
    Proofview.Goal.enter { enter = fun gl ->
      let env = Proofview.Goal.env gl in
@@ -405,8 +411,8 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
              let tac =
                with_prods nprods poly (term,cl)
                           ({ enter = fun gl clenv ->
-                             (matches_pattern concl p) <*>
-                               ((unify_resolve_refine poly flags).enter gl clenv)})
+                             matches_pattern concl p <*>
+                               unify_resolve_refine poly flags gl clenv})
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -420,8 +426,8 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
            if get_typeclasses_filtered_unification () then
              let tac = (with_prods nprods poly (term,cl)
                   ({ enter = fun gl clenv ->
-                             (matches_pattern concl p) <*>
-                               ((unify_resolve_refine poly flags).enter gl clenv)})) in
+                             matches_pattern concl p <*>
+                             unify_resolve_refine poly flags gl clenv})) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -431,7 +437,15 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
              else
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
-      | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+        | Give_exact (c,clenv) ->
+           if get_typeclasses_filtered_unification () then
+             let tac =
+               matches_pattern concl p <*>
+                 Proofview.Goal.nf_enter
+                   { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
+             Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
+           else
+             Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
       | Res_pf_THEN_trivial_fail (term,cl) ->
          let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
-- 
cgit v1.2.3


From 59b4938c3a763e0ed35dd8f91f5d45b286df01a6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Oct 2016 18:32:31 +0200
Subject: TCS: error handling and debug printing in resolution

---
 tactics/class_tactics.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 264df52154..8ec005a601 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1044,13 +1044,18 @@ module Search = struct
     let foundone = ref false in
     let rec onetac e (tac, pat, b, name, pp) tl =
       let derivs = path_derivate info.search_cut name in
-      (if !typeclasses_debug > 1 then
-         Feedback.msg_debug
-           (pr_depth (!idx :: info.search_depth) ++ str": trying " ++
+      let pr_error ie =
+        if !typeclasses_debug > 1 then
+          let msg =
+            pr_depth (!idx :: info.search_depth) ++ str": " ++
               Lazy.force pp ++
               (if !foundone != true then
                  str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
-               else mt ())));
+               else mt ())
+          in
+          Feedback.msg_debug (msg ++ str " failed with " ++ CErrors.iprint ie)
+        else ()
+      in
       let tac_of gls i j = Goal.nf_enter { enter = fun gl' ->
         let sigma' = Goal.sigma gl' in
         let s' = Sigma.to_evar_map sigma' in
@@ -1136,7 +1141,9 @@ module Search = struct
       else ortac
              (with_shelf tac >>= fun s ->
               let i = !idx in incr idx; result s i None)
-             (fun e' -> aux (merge_exceptions e e') tl)
+             (fun e' -> if CErrors.noncritical (fst e') then
+                       (pr_error e'; aux (merge_exceptions e e') tl)
+                     else iraise e')
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
-- 
cgit v1.2.3


From 8aa945902d40765f69cd16ce7647d3c28248eb54 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Oct 2016 18:33:08 +0200
Subject: Handle Unique Solutions flag.

---
 tactics/class_tactics.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 8ec005a601..c1a2f7ff2f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -9,7 +9,6 @@
 (* TODO:
   - Find an interface allowing eauto to backtrack when shelved goals remain,
    e.g. to force instantiations.
-  - unique solutions
  *)
 
 open Pp
@@ -1256,6 +1255,9 @@ module Search = struct
          Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
                                     (if Option.is_empty depth then mt()
                                      else str" without reaching its limit"))
+      | Proofview.MoreThanOneSuccess ->
+         Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
+                                  str"more than one success found.")
       | e -> Proofview.tclZERO ~info:ie e
     in Proofview.tclOR tac error
 
@@ -1273,6 +1275,11 @@ module Search = struct
        let _, pv = Proofview.init evm' [] in
        let pv = Proofview.unshelve goals pv in
        try
+         let tac =
+           if unique then
+             Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
+           else tac
+         in
          let (), pv', (unsafe, shelved, gaveup), _ =
            Proofview.apply (Global.env ()) tac pv
          in
@@ -1292,7 +1299,7 @@ module Search = struct
        with Logic_monad.TacticFailure _ -> raise Not_found
 
   let eauto depth only_classes unique dep st hints p evd =
-    let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep hints in
+    let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep:(unique || dep) hints in
     let res = run_on_evars ~unique p evd eauto_tac in
     match res with
     | None -> evd
-- 
cgit v1.2.3


From a477dca64bb71a98fb92875df438d44d1fe54400 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 26 Oct 2016 19:20:08 +0200
Subject: Fix handling of only_classes at toplevel

---
 tactics/class_tactics.ml  | 99 ++++++++++++++++++++++++++++++++---------------
 tactics/class_tactics.mli |  2 +
 2 files changed, 69 insertions(+), 32 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c1a2f7ff2f..103368e022 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -92,7 +92,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
-      optdepr  = false;
+      optdepr  = true;
       optname  = "do typeclass search modulo eta conversion";
       optkey   = ["Typeclasses";"Modulo";"Eta"];
       optread  = get_typeclasses_modulo_eta;
@@ -183,8 +183,8 @@ let set_typeclasses_depth =
 type search_strategy = Dfs | Bfs
 
 let set_typeclasses_strategy = function
-  | Dfs -> set_typeclasses_iterative_deepening true
-  | Bfs -> set_typeclasses_iterative_deepening false
+  | Dfs -> set_typeclasses_iterative_deepening false
+  | Bfs -> set_typeclasses_iterative_deepening true
 
 let pr_ev evs ev =
   Printer.pr_constr_env (Goal.V82.env evs ev) evs
@@ -302,7 +302,7 @@ let with_prods nprods poly (c, clenv) f =
           | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
           | Some (diff, clenv') -> f.enter gl (c, diff, clenv')
       with e when CErrors.noncritical e ->
-        Tacticals.New.tclFAIL 0 (CErrors.print e) end }
+        Tacticals.New.tclZEROMSG (CErrors.print e) end }
   else Proofview.Goal.nf_enter
          { enter = begin fun gl ->
                    if Int.equal nprods 0 then f.enter gl (c, None, clenv)
@@ -345,8 +345,8 @@ let pr_gls sigma gls =
 let shelve_dependencies gls =
   let open Proofview in
   tclEVARMAP >>= fun sigma ->
-  (if !typeclasses_debug > 1 then
-     Feedback.msg_debug (str" shelving goals: " ++ pr_gls sigma gls);
+  (if !typeclasses_debug > 1 && List.length gls > 0 then
+     Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls);
    shelve_goals gls)
 
 (** Hack to properly solve dependent evars that are typeclasses *)
@@ -1011,6 +1011,17 @@ module Search = struct
 	Evd.add sigma gl evi')
       sigma goals
 
+  let shelve_nonclass info =
+    Proofview.Goal.enter { enter = fun gl ->
+      let gl = Proofview.Goal.assume gl in
+      let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+      if is_class_type sigma (Proofview.Goal.concl gl) then
+        Proofview.tclUNIT ()
+      else (if !typeclasses_debug > 1 then
+              Feedback.msg_debug (pr_depth info.search_depth ++ str": shelving non-class subgoal " ++
+                                    pr_ev sigma (Proofview.Goal.goal gl));
+            Proofview.shelve) }
+
   (** The general hint application tactic.
       tac1 + tac2 .... The choice of OR or ORELSE is determined
       depending on the dependencies of the goal and the unique/Prop
@@ -1121,7 +1132,7 @@ module Search = struct
                in the subgoals, turn them into subgoals now. *)
             let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in
             let shelved = List.map fst shelved and goals = List.map fst goals in
-            if !typeclasses_debug > 1 then
+            if !typeclasses_debug > 1 && not (List.is_empty goals) then
               Feedback.msg_debug
                 (str"Adding shelved subgoals to the search: " ++
                  prlist_with_sep spc (pr_ev sigma) goals ++
@@ -1137,12 +1148,18 @@ module Search = struct
         in res <*> tclEVARMAP >>= finish
       in
       if path_matches derivs [] then aux e tl
-      else ortac
-             (with_shelf tac >>= fun s ->
+      else
+        let filter =
+          if info.search_only_classes then shelve_nonclass info
+          else Proofview.tclUNIT ()
+        in
+        ortac
+             (with_shelf (tac <*> filter) >>= fun s ->
               let i = !idx in incr idx; result s i None)
-             (fun e' -> if CErrors.noncritical (fst e') then
-                       (pr_error e'; aux (merge_exceptions e e') tl)
-                     else iraise e')
+             (fun e' ->
+	      if CErrors.noncritical (fst e') then
+                (pr_error e'; aux (merge_exceptions e e') tl)
+              else (Printf.printf "raising again\n%!"; iraise e'))
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
@@ -1203,9 +1220,12 @@ module Search = struct
         unit Proofview.tactic =
     let open Proofview in
     let open Proofview.Notations in
-    let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
-    let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
-    search_tac hints depth 1 info
+    if only_classes && not (is_class_type sigma (Goal.concl gl)) then
+      Proofview.shelve
+    else
+      let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+      let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+      search_tac hints depth 1 info
 
   let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
     let open Proofview in
@@ -1236,7 +1256,22 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let eauto_tac ?(st=full_transparent_state) ~only_classes ~depth ~dep hints =
+  let disallow_shelved tac =
+    let open Proofview in
+    with_shelf (tclONCE tac) >>= fun (shelved,result) ->
+    (if not (List.is_empty shelved) then
+       begin
+         Proofview.tclEVARMAP >>= fun sigma ->
+	 let gls = prlist_with_sep spc (pr_ev sigma) shelved in
+	 (if !typeclasses_debug > 0 then
+	  Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls));
+	 Tacticals.New.tclFAIL 1 (str"Proof search failed: " ++
+				  str"shelved goals remain: " ++ gls)
+       end
+     else tclUNIT result)
+
+  let eauto_tac ?(st=full_transparent_state) ?(unique=false) ~only_classes ~depth ~dep hints =
+    let open Proofview in
     let tac =
       let search = search_tac ~st only_classes dep hints in
       if get_typeclasses_iterative_deepening () then
@@ -1257,11 +1292,19 @@ module Search = struct
                                      else str" without reaching its limit"))
       | Proofview.MoreThanOneSuccess ->
          Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
-                                  str"more than one success found.")
+                                  str"more than one success found")
       | e -> Proofview.tclZERO ~info:ie e
-    in Proofview.tclOR tac error
+    in
+    let tac = Proofview.tclOR tac error in
+    let tac =
+      if unique then
+        Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
+      else tac
+    in
+    let tac = if only_classes then disallow_shelved tac else tac in
+    tac
 
-  let run_on_evars ?(unique=false) p evm tac =
+  let run_on_evars p evm tac =
     match evars_to_goals p evm with
     | None -> None (* This happens only because there's no evar having p *)
     | Some (goals, evm') ->
@@ -1275,11 +1318,6 @@ module Search = struct
        let _, pv = Proofview.init evm' [] in
        let pv = Proofview.unshelve goals pv in
        try
-         let tac =
-           if unique then
-             Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
-           else tac
-         in
          let (), pv', (unsafe, shelved, gaveup), _ =
            Proofview.apply (Global.env ()) tac pv
          in
@@ -1298,16 +1336,15 @@ module Search = struct
          else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
 
-  let eauto depth only_classes unique dep st hints p evd =
-    let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep:(unique || dep) hints in
-    let res = run_on_evars ~unique p evd eauto_tac in
+  let evars_eauto depth only_classes unique dep st hints p evd =
+    let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+    let res = run_on_evars p evd eauto_tac in
     match res with
     | None -> evd
     | Some evd' -> evd'
-  (* TODO treat unique solutions *)
 
   let typeclasses_eauto ?depth unique st hints p evd =
-    eauto depth true unique false st hints p evd
+    evars_eauto depth true unique false st hints p evd
   (** Typeclasses eauto is an eauto which tries to resolve only
       goals of typeclass type, and assumes that the initially selected
       evars in evd are independent of the rest of the evars *)
@@ -1318,8 +1355,6 @@ module Search = struct
 end
 
 (** Binding to either V85 or Search implementations. *)
-let eauto depth ~only_classes ~st ~dep dbs =
-  Search.eauto_tac ~st ~only_classes ~depth ~dep dbs
 
 let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
                       ~depth dbs =
@@ -1336,7 +1371,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
       try V85.eauto85 depth ~only_classes ~st dbs gl
       with Not_found ->
 	Refiner.tclFAIL 0 (str"Proof search failed") gl)
-  else eauto depth ~only_classes ~st ~dep:true dbs
+  else Search.eauto_tac ~st ~only_classes ~depth ~dep:true dbs
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 565415a95e..21c5d2172b 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -40,6 +40,8 @@ module Search : sig
   val eauto_tac :
     ?st:Names.transparent_state ->
     (** The transparent_state used when working with local hypotheses  *)
+    ?unique:bool ->
+    (** Should we force a unique solution *)
     only_classes:bool ->
     (** Should non-class goals be shelved and resolved at the end *)
     depth:Int.t option ->
-- 
cgit v1.2.3


From c0f3d5fb81c543d1b05b0ff7041efee086514f3a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 11:48:26 +0200
Subject: Fix [typeclasses eauto with] and nopattern hints

This was the source of a bug in #5115#c7.
---
 tactics/class_tactics.ml | 39 ++++++++++++++++++++++++---------------
 1 file changed, 24 insertions(+), 15 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 103368e022..72e410160d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -349,6 +349,15 @@ let shelve_dependencies gls =
      Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls);
    shelve_goals gls)
 
+let hintmap_of hdc secvars concl =
+  match hdc with
+  | None -> fun db -> Hint_db.map_none secvars db
+  | Some hdc ->
+     fun db ->
+     if Hint_db.use_dn db then (* Using dnet *)
+       Hint_db.map_eauto secvars hdc concl db
+     else Hint_db.map_existential secvars hdc concl db
+
 (** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db secvars =
   let open Tacticals.New in
@@ -384,20 +393,20 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
   let nprods = List.length prods in
   let freeze =
     try
-      let cl = Typeclasses.class_info (fst hdc) in
-        if cl.cl_strict then
-          Evd.evars_of_term concl
-        else Evar.Set.empty
+      match hdc with
+      | Some (hd,_) when only_classes ->
+         let cl = Typeclasses.class_info hd in
+         if cl.cl_strict then
+           Evd.evars_of_term concl
+         else Evar.Set.empty
+      | _ -> Evar.Set.empty
     with e when CErrors.noncritical e -> Evar.Set.empty
   in
+  let hint_of_db = hintmap_of hdc secvars concl in
   let hintl =
     List.map_append
       (fun db ->
-        let tacs =
-          if Hint_db.use_dn db then (* Using dnet *)
-            Hint_db.map_eauto secvars hdc concl db
-          else Hint_db.map_existential secvars hdc concl db
-        in
+        let tacs = hint_of_db db in
         let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
           List.map (fun x -> (flags, x)) tacs)
       (local_db::db_list)
@@ -469,16 +478,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
+  let hd = try Some (decompose_app_bound concl) with Bound -> None in
   try
-    e_my_find_search db_list local_db secvars
-     (decompose_app_bound concl) true only_classes sigma concl
-  with Bound | Not_found -> []
+    e_my_find_search db_list local_db secvars hd true only_classes sigma concl
+  with Not_found -> []
 
 let e_possible_resolve db_list local_db secvars only_classes sigma concl =
+  let hd = try Some (decompose_app_bound concl) with Bound -> None in
   try
-    e_my_find_search db_list local_db secvars
-      (decompose_app_bound concl) false only_classes sigma concl
-  with Bound | Not_found -> []
+    e_my_find_search db_list local_db secvars hd false only_classes sigma concl
+  with Not_found -> []
 
 let cut_of_hints h =
   List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
-- 
cgit v1.2.3


From 98305374e2fdec4b64d7d086ddca0c4e812b178e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 11:51:38 +0200
Subject: typeclasses eauto Implem/doc of shelving strategy

Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
---
 tactics/class_tactics.ml | 47 ++++++++++++++++++++++++++++++++---------------
 1 file changed, 32 insertions(+), 15 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 72e410160d..91eb388b3e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1265,21 +1265,29 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let disallow_shelved tac =
+  let disallow_shelved initshelf tac =
     let open Proofview in
-    with_shelf (tclONCE tac) >>= fun (shelved,result) ->
-    (if not (List.is_empty shelved) then
-       begin
-         Proofview.tclEVARMAP >>= fun sigma ->
-	 let gls = prlist_with_sep spc (pr_ev sigma) shelved in
-	 (if !typeclasses_debug > 0 then
-	  Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls));
-	 Tacticals.New.tclFAIL 1 (str"Proof search failed: " ++
-				  str"shelved goals remain: " ++ gls)
-       end
-     else tclUNIT result)
-
-  let eauto_tac ?(st=full_transparent_state) ?(unique=false) ~only_classes ~depth ~dep hints =
+    let casefn = function
+    | Fail (e,info) -> tclZERO ~info e
+    | Next ((shelved, result), k) ->
+       if not (List.is_empty shelved) then
+         begin
+           Proofview.tclEVARMAP >>= fun sigma ->
+	   let gls = prlist_with_sep spc (pr_ev sigma) shelved in
+	   (if !typeclasses_debug > 0 then
+	      let initgls = prlist_with_sep spc (pr_ev sigma) initshelf in
+	      Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls
+                                  ++ str" initially: " ++ initgls ++ str"."));
+	   Tacticals.New.tclZEROMSG (str"Proof search failed: " ++
+				      str"shelved goals remain: " ++ gls)
+         end
+       else
+         tclOR (tclUNIT result) (fun e -> k e >>= fun (gls, result) -> tclUNIT result)
+    in
+    tclCASE (with_shelf tac) >>= casefn
+
+  let eauto_tac ?(st=full_transparent_state) ?(unique=false)
+                ~only_classes ~depth ~dep hints =
     let open Proofview in
     let tac =
       let search = search_tac ~st only_classes dep hints in
@@ -1310,7 +1318,16 @@ module Search = struct
         Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
       else tac
     in
-    let tac = if only_classes then disallow_shelved tac else tac in
+    with_shelf numgoals >>= fun (initshelf, i) ->
+    (if !typeclasses_debug > 1 then
+       Feedback.msg_debug (str"Starting resolution with " ++ int i ++
+                             str" goal(s) under focus and " ++
+                             int (List.length initshelf) ++ str " shelved goal(s)" ++
+                             if only_classes then str " in only_classes mode" else
+                               str " in regular mode" ++
+                                 match depth with None -> str ", unbounded"
+                                                | Some i -> str ", with depth limit " ++ int i));
+    let tac = if only_classes then disallow_shelved initshelf tac else tac in
     tac
 
   let run_on_evars p evm tac =
-- 
cgit v1.2.3


From f6916774eea2ecc1262377cb14c2d494a0486358 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 19:07:21 +0200
Subject: Do not shelve non-class subgoals but fail, it should

be the instance writer's responsibility to not generated non-dependent
non-class subgoals (otherwise we loose compatibility as shown in
e.g. MathClasses, which goes into loops because of unexpectedly
unconstrained goals). Reflect it in the doc.
---
 tactics/class_tactics.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 91eb388b3e..fe12b54a13 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1020,16 +1020,17 @@ module Search = struct
 	Evd.add sigma gl evi')
       sigma goals
 
-  let shelve_nonclass info =
+  let fail_if_nonclass info =
     Proofview.Goal.enter { enter = fun gl ->
       let gl = Proofview.Goal.assume gl in
       let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
       if is_class_type sigma (Proofview.Goal.concl gl) then
         Proofview.tclUNIT ()
       else (if !typeclasses_debug > 1 then
-              Feedback.msg_debug (pr_depth info.search_depth ++ str": shelving non-class subgoal " ++
+              Feedback.msg_debug (pr_depth info.search_depth ++
+                                    str": failure due to non-class subgoal " ++
                                     pr_ev sigma (Proofview.Goal.goal gl));
-            Proofview.shelve) }
+            Proofview.tclZERO NotApplicableEx) }
 
   (** The general hint application tactic.
       tac1 + tac2 .... The choice of OR or ORELSE is determined
@@ -1159,7 +1160,7 @@ module Search = struct
       if path_matches derivs [] then aux e tl
       else
         let filter =
-          if info.search_only_classes then shelve_nonclass info
+          if info.search_only_classes then fail_if_nonclass info
           else Proofview.tclUNIT ()
         in
         ortac
-- 
cgit v1.2.3


From 919545d39c77a9168e70141e78d2c9589dad7c4e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 27 Oct 2016 14:14:50 +0200
Subject: Internal API change to typeclasses eauto.

This commit makes the traversing strategy of typeclasses
eauto an optional argument of the function that implements
it.
This change should be non-breaking.
---
 tactics/class_tactics.ml  | 9 +++++++--
 tactics/class_tactics.mli | 3 +++
 2 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fe12b54a13..5d5511d78f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1288,11 +1288,16 @@ module Search = struct
     tclCASE (with_shelf tac) >>= casefn
 
   let eauto_tac ?(st=full_transparent_state) ?(unique=false)
-                ~only_classes ~depth ~dep hints =
+                ~only_classes ?dfs ~depth ~dep hints =
     let open Proofview in
     let tac =
       let search = search_tac ~st only_classes dep hints in
-      if get_typeclasses_iterative_deepening () then
+      let bfs =
+        match dfs with
+        | None -> get_typeclasses_iterative_deepening ()
+        | Some v -> v
+      in
+      if bfs then
         match depth with
         | None -> fix_iterative search
         | Some l -> fix_iterative_limit l search
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 21c5d2172b..1b2fa035bd 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -44,6 +44,9 @@ module Search : sig
     (** Should we force a unique solution *)
     only_classes:bool ->
     (** Should non-class goals be shelved and resolved at the end *)
+    ?dfs:bool ->
+    (** Is a traversing-strategy specified?
+        If yes, true means dfs, false means bfs, i.e iterative deepening *)
     depth:Int.t option ->
     (** Bounded or unbounded search *)
     dep:bool ->
-- 
cgit v1.2.3


From a4cecc13cde3239d6a86f98ba6bba0e4554306bd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 3 Nov 2016 16:25:06 +0100
Subject: Rework search_strategy option handling

---
 tactics/class_tactics.ml  | 64 ++++++++++++++++++++++++++---------------------
 tactics/class_tactics.mli |  7 +++---
 2 files changed, 39 insertions(+), 32 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 5d5511d78f..63994bafe6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -914,19 +914,20 @@ module V85 = struct
   let eauto_tac hints =
     then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
 
-  let eauto_tac depth hints =
-    if get_typeclasses_iterative_deepening () then
-      match depth with
-      | None -> fix_iterative (eauto_tac hints)
-      | Some depth -> fix_iterative_limit depth (eauto_tac hints)
-    else
-      match depth with
-      | None -> fix (eauto_tac hints)
-      | Some depth -> fix_limit depth (eauto_tac hints)
-
-  let real_eauto ?depth unique st hints p evd =
+  let eauto_tac strategy depth hints =
+    match strategy with
+    | Bfs -> 
+       begin match depth with
+       | None -> fix_iterative (eauto_tac hints)
+       | Some depth -> fix_iterative_limit depth (eauto_tac hints) end
+    | Dfs ->
+       match depth with
+       | None -> fix (eauto_tac hints)
+       | Some depth -> fix_limit depth (eauto_tac hints)
+                                
+  let real_eauto ?depth strategy unique st hints p evd =
     let res =
-      run_on_evars ~st ~unique p evd hints (eauto_tac depth hints)
+      run_on_evars ~st ~unique p evd hints (eauto_tac strategy depth hints)
     in
     match res with
     | None -> evd
@@ -939,12 +940,18 @@ module V85 = struct
 
   let resolve_all_evars_once debug depth unique p evd =
     let db = searchtable_map typeclasses_db in
-    real_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd
-
-  let eauto85 ?(only_classes=true) ?st depth hints g =
+    let strategy = if get_typeclasses_iterative_deepening () then Bfs else Dfs in
+    real_eauto ?depth strategy unique (Hint_db.transparent_state db) [db] p evd
+
+  let eauto85 ?(only_classes=true) ?st ?strategy depth hints g =
+    let strategy =
+      match strategy with
+      | None -> if get_typeclasses_iterative_deepening () then Bfs else Dfs
+      | Some s -> s
+    in
     let gl = { it = make_autogoal ~only_classes ?st
                                   (cut_of_hints hints) None g; sigma = project g; } in
-    match run_tac (eauto_tac depth hints) gl with
+    match run_tac (eauto_tac strategy depth hints) gl with
     | None -> raise Not_found
     | Some {it = goals; sigma = s; } ->
        {it = List.map fst goals; sigma = s;}
@@ -1288,22 +1295,23 @@ module Search = struct
     tclCASE (with_shelf tac) >>= casefn
 
   let eauto_tac ?(st=full_transparent_state) ?(unique=false)
-                ~only_classes ?dfs ~depth ~dep hints =
+                ~only_classes ?strategy ~depth ~dep hints =
     let open Proofview in
     let tac =
       let search = search_tac ~st only_classes dep hints in
-      let bfs =
-        match dfs with
-        | None -> get_typeclasses_iterative_deepening ()
-        | Some v -> v
+      let dfs =
+        match strategy with
+        | None -> not (get_typeclasses_iterative_deepening ())
+        | Some Dfs -> true
+        | Some Bfs -> false
       in
-      if bfs then
+      if dfs then
+        let depth = match depth with None -> -1 | Some d -> d in
+        search depth
+      else
         match depth with
         | None -> fix_iterative search
         | Some l -> fix_iterative_limit l search
-      else
-        let depth = match depth with None -> -1 | Some d -> d in
-        search depth
     in
     let error (e, ie) =
       match e with
@@ -1389,7 +1397,7 @@ end
 (** Binding to either V85 or Search implementations. *)
 
 let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
-                      ~depth dbs =
+                      ?strategy ~depth dbs =
   let dbs = List.map_filter
               (fun db -> try Some (searchtable_map db)
                       with e when CErrors.noncritical e -> None)
@@ -1400,10 +1408,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
   if get_typeclasses_legacy_resolution () then
     Proofview.V82.tactic
     (fun gl ->
-      try V85.eauto85 depth ~only_classes ~st dbs gl
+      try V85.eauto85 depth ~only_classes ~st ?strategy dbs gl
       with Not_found ->
 	Refiner.tclFAIL 0 (str"Proof search failed") gl)
-  else Search.eauto_tac ~st ~only_classes ~depth ~dep:true dbs
+  else Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 1b2fa035bd..76760db025 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -24,7 +24,7 @@ type search_strategy = Dfs | Bfs
 
 val set_typeclasses_strategy : search_strategy -> unit
 
-val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
+val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy ->
                         depth:(Int.t option) ->
                         Hints.hint_db_name list -> unit Proofview.tactic
 
@@ -44,9 +44,8 @@ module Search : sig
     (** Should we force a unique solution *)
     only_classes:bool ->
     (** Should non-class goals be shelved and resolved at the end *)
-    ?dfs:bool ->
-    (** Is a traversing-strategy specified?
-        If yes, true means dfs, false means bfs, i.e iterative deepening *)
+    ?strategy:search_strategy ->
+    (** Is a traversing-strategy specified? *)
     depth:Int.t option ->
     (** Bounded or unbounded search *)
     dep:bool ->
-- 
cgit v1.2.3


From 6bb352a6743c7332b9715ac15e95c806a58d101c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Nov 2016 14:55:40 +0100
Subject: Fix refine in compatibility mode

---
 tactics/tactics.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d2e5d8525d..548d2a81f3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4973,9 +4973,15 @@ module New = struct
   open Locus
 
   let reduce_after_refine =
+    let onhyps =
+      (** We reduced everywhere in the hyps before 8.6 *)
+      if Flags.version_less_or_equal Flags.V8_5 then None
+      else Some []
+    in
     reduce
-      (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=None; concl_occs=AllOccurrences }
+      (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;
+	     rZeta=false;rDelta=false;rConst=[]})
+      {onhyps; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
     Refine.refine ?unsafe c <*>
-- 
cgit v1.2.3


From 22dfbff296cf03b6fab2bcec4eb5f9cf6ee8368c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Nov 2016 15:55:52 +0100
Subject: Fix #3441 Use pf_get_type_of to avoid blowup

... in pose proof of large proof terms
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 548d2a81f3..92cb8a11ea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2714,7 +2714,7 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter { enter = begin fun gl ->
-      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let t = Tacmach.New.pf_get_type_of gl c in
       let hd = head_ident c in
       Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
       end }
-- 
cgit v1.2.3


From d8baa76d86eaa691a5386669596a6004bb44bb7a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Nov 2016 18:00:18 +0100
Subject: More precise refine compatibility

---
 tactics/tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 92cb8a11ea..af52c52370 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4975,7 +4975,8 @@ module New = struct
   let reduce_after_refine =
     let onhyps =
       (** We reduced everywhere in the hyps before 8.6 *)
-      if Flags.version_less_or_equal Flags.V8_5 then None
+      if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0
+      then None
       else Some []
     in
     reduce
-- 
cgit v1.2.3


From e6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 7 Nov 2016 08:41:21 +0100
Subject: More explicit name for status of unification constraints.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 893f33f1a8..e8cf09415c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1141,7 +1141,7 @@ let run_delayed env sigma c =
 
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
+  Pretyping.solve_unification_constraints = true;
   Pretyping.use_hook = Some solve_by_implicit_tactic;
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
-- 
cgit v1.2.3


From 1f36cdefd841526f804bd2dd51c1d88309333376 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 14:47:15 +0100
Subject: Fixes to compile with ocaml 4.01

---
 tactics/hints.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9cbfe20d96..53573bc7e4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -84,7 +84,9 @@ let secvars_of_hyps hyps =
   if all then Id.Pred.full (* If the whole section context is available *)
   else pred
 
-let empty_hint_info = Vernacexpr.{ hint_priority = None; hint_pattern = None }
+let empty_hint_info =
+  let open Vernacexpr in
+  { hint_priority = None; hint_pattern = None }
 
 (************************************************************************)
 (*           The Type of Constructions Autotactic Hints                 *)
-- 
cgit v1.2.3


From 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 15 Nov 2016 13:53:57 +0100
Subject: Revert part of a477dc, disallow_shelved

In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.

Fix test-suite now that shelved goals are allowed
---
 tactics/class_tactics.ml | 24 +-----------------------
 1 file changed, 1 insertion(+), 23 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 262b308932..99a1a98993 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1176,7 +1176,7 @@ module Search = struct
              (fun e' ->
 	      if CErrors.noncritical (fst e') then
                 (pr_error e'; aux (merge_exceptions e e') tl)
-              else (Printf.printf "raising again\n%!"; iraise e'))
+              else iraise e')
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
@@ -1274,27 +1274,6 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let disallow_shelved initshelf tac =
-    let open Proofview in
-    let casefn = function
-    | Fail (e,info) -> tclZERO ~info e
-    | Next ((shelved, result), k) ->
-       if not (List.is_empty shelved) then
-         begin
-           Proofview.tclEVARMAP >>= fun sigma ->
-	   let gls = prlist_with_sep spc (pr_ev sigma) shelved in
-	   (if !typeclasses_debug > 0 then
-	      let initgls = prlist_with_sep spc (pr_ev sigma) initshelf in
-	      Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls
-                                  ++ str" initially: " ++ initgls ++ str"."));
-	   Tacticals.New.tclZEROMSG (str"Proof search failed: " ++
-				      str"shelved goals remain: " ++ gls)
-         end
-       else
-         tclOR (tclUNIT result) (fun e -> k e >>= fun (gls, result) -> tclUNIT result)
-    in
-    tclCASE (with_shelf tac) >>= casefn
-
   let eauto_tac ?(st=full_transparent_state) ?(unique=false)
                 ~only_classes ?strategy ~depth ~dep hints =
     let open Proofview in
@@ -1342,7 +1321,6 @@ module Search = struct
                                str " in regular mode" ++
                                  match depth with None -> str ", unbounded"
                                                 | Some i -> str ", with depth limit " ++ int i));
-    let tac = if only_classes then disallow_shelved initshelf tac else tac in
     tac
 
   let run_on_evars p evm tac =
-- 
cgit v1.2.3


From 09fd1e8b5e810bae0e50ecd4901cd7c8f1464f4a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 16 Nov 2016 10:45:25 +0100
Subject: Revert more of a477dc for good measure

We stop failing automatically on non-declared-class nested or toplevel
subgoals as in 8.5, instead of the previous a477dc behavior of shelving
those goals and failing if shelved goals remained at the end of
resolution. It means typeclass resolution during refinement is closer to
all:typeclasses eauto. Hints in typeclass_instances for non-declared
classes can be used during resolution of _nested_ subgoals when it is
fired from type-inference, toplevel goals considered in this case are
still only classes (as in 8.5 and before). The code that triggers the
restriction to only declared class subgoals is commented.

Revert changes to test-suite, adding test for #5203, #5198 is fixed too.

Add corresponding tests in the test-suite (that will break if we,
e.g. disallow non-class subgoals) and update the refman accordingly.
---
 tactics/class_tactics.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 99a1a98993..4138562c64 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1167,7 +1167,8 @@ module Search = struct
       if path_matches derivs [] then aux e tl
       else
         let filter =
-          if info.search_only_classes then fail_if_nonclass info
+          if false (* in 8.6, still allow non-class subgoals
+                    info.search_only_classes *) then fail_if_nonclass info
           else Proofview.tclUNIT ()
         in
         ortac
@@ -1238,8 +1239,8 @@ module Search = struct
         unit Proofview.tactic =
     let open Proofview in
     let open Proofview.Notations in
-    if only_classes && not (is_class_type sigma (Goal.concl gl)) then
-      Proofview.shelve
+    if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
+      Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
       let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
       let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
-- 
cgit v1.2.3


From 37e0ce25f88a77c48c480e37ccca444a8f5fe4e8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 16 Nov 2016 16:22:53 +0100
Subject: Minor debug printing bug,

Hit by OCaml's "if then else" with no "end" once more
---
 tactics/class_tactics.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4138562c64..e44ace4257 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1318,10 +1318,9 @@ module Search = struct
        Feedback.msg_debug (str"Starting resolution with " ++ int i ++
                              str" goal(s) under focus and " ++
                              int (List.length initshelf) ++ str " shelved goal(s)" ++
-                             if only_classes then str " in only_classes mode" else
-                               str " in regular mode" ++
-                                 match depth with None -> str ", unbounded"
-                                                | Some i -> str ", with depth limit " ++ int i));
+                             (if only_classes then str " in only_classes mode" else str " in regular mode") ++
+                             match depth with None -> str ", unbounded"
+                                            | Some i -> str ", with depth limit " ++ int i));
     tac
 
   let run_on_evars p evm tac =
-- 
cgit v1.2.3