Merge branch 'v8.6'

5 files changed, 51 insertions, 18 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 8ea60b39ae..2225650204 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -37,7 +37,7 @@ DECLARE PLUGIN "extratactics"
 let with_delayed_uconstr ist c tac =
   let flags = {
     Pretyping.use_typeclasses = false;
-    use_unif_heuristics = true;
+    solve_unification_constraints = true;
     use_hook = Some Pfedit.solve_by_implicit_tactic;
     fail_evar = false;
     expand_evars = true
@@ -315,7 +315,8 @@ let project_hint pri l2r r =
   in
   let ctx = Evd.universe_context_set sigma in
   let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
-    (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
+  let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
+    (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
 let add_hints_iff l2r lc n bl =
   Hints.add_hints true bl
@@ -341,16 +342,17 @@ END
 
 let constr_flags = {
   Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
+  Pretyping.solve_unification_constraints = true;
   Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
 
-let refine_tac ist simple c =
+let refine_tac ist simple with_classes c =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let flags = constr_flags in
+    let flags =
+      { constr_flags with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
@@ -362,11 +364,28 @@ let refine_tac ist simple c =
   end }
 
 TACTIC EXTEND refine
-| [ "refine" uconstr(c) ] -> [ refine_tac ist false c ]
+| [ "refine" uconstr(c) ] ->
+   [ refine_tac ist false true c ]
 END
 
 TACTIC EXTEND simple_refine
-| [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ]
+| [ "simple" "refine" uconstr(c) ] ->
+   [ refine_tac ist true true c ]
+END
+
+TACTIC EXTEND notcs_refine
+| [ "notypeclasses" "refine" uconstr(c) ] ->
+   [ refine_tac ist false false c ]
+END
+
+TACTIC EXTEND notcs_simple_refine
+| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
+   [ refine_tac ist true false c ]
+END
+
+(* Solve unification constraints using heuristics or fail if any remain *)
+TACTIC EXTEND solve_constraints
+[ "solve_constraints" ] -> [ Refine.solve_constraints ]
 END
 
 (**********************************************************************)
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 82ba63871e..03ef3e5c9b 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -43,7 +43,7 @@ END
 let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
-    use_unif_heuristics = true;
+    solve_unification_constraints = true;
     use_hook = Some Pfedit.solve_by_implicit_tactic;
     fail_evar = false;
     expand_evars = true
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index f8654d3903..a28132a4b0 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,19 +44,33 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
 | [ ] -> [ false ]
 END
 
+let pr_search_strategy _prc _prlc _prt = function
+  | Some Dfs -> Pp.str "dfs"
+  | Some Bfs -> Pp.str "bfs"
+  | None -> Pp.mt ()
+
+ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy
+| [ "(bfs)" ] -> [ Some Bfs ]
+| [ "(dfs)" ] -> [ Some Dfs ]
+| [ ] -> [ None ] 
+END
+
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [
      set_typeclasses_debug d;
+     Option.iter set_typeclasses_strategy s;
      set_typeclasses_depth depth
    ]
 END
 
 (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
+ | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+    [ typeclasses_eauto ~strategy:Bfs ~depth:d l ]
  | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
-    [ typeclasses_eauto d l ]
+    [ typeclasses_eauto ~depth:d l ]
  | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
      typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
 END
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 217f5f42ef..3c5a109c0d 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1791,7 +1791,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 let anew_instance global binders instance fields =
   new_instance (Flags.is_universe_polymorphism ()) 
     binders instance (Some (true, CRecord (Loc.ghost,fields)))
-    ~global ~generalize:false ~refine:false None
+    ~global ~generalize:false ~refine:false Hints.empty_hint_info
 
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
@@ -1972,7 +1972,7 @@ let add_morphism_infer glob m n =
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
-			(Lazy.force PropGlobal.proper_class) None glob 
+			(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob
 			poly (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
@@ -1983,7 +1983,7 @@ let add_morphism_infer glob m n =
       let hook _ = function
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
-			  (Lazy.force PropGlobal.proper_class) None
+			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
 			  glob poly (ConstRef cst));
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
@@ -2007,7 +2007,7 @@ let add_morphism glob binders m s n =
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
     ignore(new_instance ~global:glob poly binders instance 
 	     (Some (true, CRecord (Loc.ghost,[])))
-	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
+	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)
 
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index e927ea0642..ddeab733e5 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -644,7 +644,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
 
 let constr_flags = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = Some solve_by_implicit_tactic;
   fail_evar = true;
   expand_evars = true }
@@ -659,21 +659,21 @@ let interp_type = interp_constr_gen IsType
 
 let open_constr_use_classes_flags = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = Some solve_by_implicit_tactic;
   fail_evar = false;
   expand_evars = true }
 
 let open_constr_no_classes_flags = {
   use_typeclasses = false;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = Some solve_by_implicit_tactic;
   fail_evar = false;
   expand_evars = true }
 
 let pure_open_constr_flags = {
   use_typeclasses = false;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = false;
   expand_evars = false }