aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/extratactics.ml436
-rw-r--r--ltac/g_auto.ml436
-rw-r--r--ltac/g_class.ml418
-rw-r--r--ltac/pptactic.ml11
-rw-r--r--ltac/rewrite.ml8
-rw-r--r--ltac/tacinterp.ml8
6 files changed, 85 insertions, 32 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 8ea60b39ae..1223f6eb4b 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,10 +315,12 @@ 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
+ let l = Locality.LocalityFixme.consume () in
+ Hints.add_hints (Locality.make_module_locality l) bl
(Hints.HintsResolveEntry (List.map (project_hint n l2r) lc))
VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
@@ -341,16 +343,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 +365,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..a37cf306e1 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -43,18 +43,24 @@ 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
} in
List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
+let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
+let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob
ARGUMENT EXTEND auto_using
TYPED AS uconstr_list
PRINTED BY pr_auto_using
+ RAW_TYPED AS uconstr_list
+ RAW_PRINTED BY pr_auto_using_raw
+ GLOB_TYPED AS uconstr_list
+ GLOB_PRINTED BY pr_auto_using_glob
| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ]
| [ ] -> [ [] ]
END
@@ -171,18 +177,32 @@ TACTIC EXTEND convert_concl_no_check
| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
END
-let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
+let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
+let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
+let glob_hints_path_atom ist = Hints.glob_hints_path_atom
ARGUMENT EXTEND hints_path_atom
PRINTED BY pr_hints_path_atom
-| [ ne_global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
+
+ GLOBALIZED BY glob_hints_path_atom
+
+ RAW_PRINTED BY pr_pre_hints_path_atom
+ GLOB_PRINTED BY pr_hints_path_atom
+| [ ne_global_list(g) ] -> [ Hints.PathHints g ]
| [ "_" ] -> [ Hints.PathAny ]
END
let pr_hints_path prc prx pry c = Hints.pp_hints_path c
-
+let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c
+let glob_hints_path ist = Hints.glob_hints_path
+
ARGUMENT EXTEND hints_path
- PRINTED BY pr_hints_path
+PRINTED BY pr_hints_path
+
+GLOBALIZED BY glob_hints_path
+RAW_PRINTED BY pr_pre_hints_path
+GLOB_PRINTED BY pr_hints_path
+
| [ "(" hints_path(p) ")" ] -> [ p ]
| [ hints_path(p) "*" ] -> [ Hints.PathStar p ]
| [ "emp" ] -> [ Hints.PathEmpty ]
@@ -192,8 +212,6 @@ ARGUMENT EXTEND hints_path
| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ]
END
-let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
-
ARGUMENT EXTEND opthints
TYPED AS preident_list_opt
PRINTED BY pr_hintbases
@@ -203,7 +221,7 @@ END
VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
- let entry = Hints.HintsCutEntry p in
+ let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
(match dbnames with None -> ["core"] | Some l -> l) entry ]
END
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/pptactic.ml b/ltac/pptactic.ml
index 6230fa0606..b1a6fa63d6 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -136,7 +136,7 @@ module Make
| ConstrContext ((_,id),c) ->
hov 0
(keyword "context" ++ spc () ++ pr_id id ++ spc () ++
- str "[" ++ prlc c ++ str "]")
+ str "[ " ++ prlc c ++ str " ]")
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc c)
| ConstrTerm c when test c ->
@@ -497,7 +497,8 @@ module Make
| _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
in
pr_in
- (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
+ (prlist_with_sep (fun () -> str",")
+ (fun id -> spc () ++ pr_hyp_location pr_id id) l ++ pr_occs)
let pr_orient b = if b then mt () else str "<- "
@@ -542,9 +543,9 @@ module Make
| Subterm (b,None,a) ->
(** ppedrot: we don't make difference between [appcontext] and [context]
anymore, and the interpretation is governed by a flag instead. *)
- keyword "context" ++ str" [" ++ pr_pat a ++ str "]"
+ keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]"
| Subterm (b,Some id,a) ->
- keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+ keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]"
let pr_match_hyps pr_pat = function
| Hyp (nal,mp) ->
@@ -1083,7 +1084,7 @@ module Make
| TacNumgoals ->
keyword "numgoals"
| (TacCall _|Tacexp _ | TacGeneric _) as a ->
- keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+ hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))))
in pr_tac
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 }
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:11:36 +0000