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

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

3 files changed, 39 insertions, 11 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 2cca760c38..d88bcd7eb1 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -316,7 +316,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
@@ -347,11 +348,12 @@ let constr_flags = {
   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
@@ -363,11 +365,23 @@ 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 *)
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 18df596eb8..7e26b5d189 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 4d7c5d0e4b..44efdd383f 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1788,7 +1788,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"
@@ -1969,7 +1969,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
@@ -1980,7 +1980,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
@@ -2004,7 +2004,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 *)