aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml21
-rw-r--r--tactics/autorewrite.mli2
-rw-r--r--tactics/cbn.ml21
-rw-r--r--tactics/cbn.mli7
-rw-r--r--tactics/class_tactics.ml3
-rw-r--r--tactics/dune2
-rw-r--r--tactics/elim.ml52
-rw-r--r--tactics/elim.mli1
-rw-r--r--tactics/hints.ml190
-rw-r--r--tactics/hints.mli2
-rw-r--r--tactics/redexpr.ml20
-rw-r--r--tactics/tactics.ml184
-rw-r--r--tactics/tactics.mli9
13 files changed, 267 insertions, 247 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index cc56de066d..1d876537ef 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -206,9 +206,15 @@ let subst_hintrewrite (subst,(rbase,list as node)) =
(rbase,list')
(* Declaration of the Hint Rewrite library object *)
-let inHintRewrite : string * HintDN.t -> Libobject.obj =
+let inGlobalHintRewrite : string * HintDN.t -> Libobject.obj =
let open Libobject in
- declare_object @@ superglobal_object_nodischarge "HINT_REWRITE"
+ declare_object @@ superglobal_object_nodischarge "HINT_REWRITE_GLOBAL"
+ ~cache:cache_hintrewrite
+ ~subst:(Some subst_hintrewrite)
+
+let inExportHintRewrite : string * HintDN.t -> Libobject.obj =
+ let open Libobject in
+ declare_object @@ global_object_nodischarge "HINT_REWRITE_EXPORT"
~cache:cache_hintrewrite
~subst:(Some subst_hintrewrite)
@@ -250,7 +256,8 @@ let find_applied_relation ?loc env sigma c left2right =
spc () ++ str"of this term does not end with an applied relation.")
(* To add rewriting rules to a base *)
-let add_rew_rules base lrul =
+let add_rew_rules ~locality base lrul =
+ let () = Hints.check_hint_locality locality in
let counter = ref 0 in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -267,5 +274,9 @@ let add_rew_rules base lrul =
rew_tac = Option.map intern t}
in incr counter;
HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
- in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
-
+ in
+ let open Goptions in
+ match locality with
+ | OptLocal -> cache_hintrewrite ((),(base,lrul))
+ | OptDefault | OptGlobal -> Lib.add_anonymous_leaf (inGlobalHintRewrite (base,lrul))
+ | OptExport -> Lib.add_anonymous_leaf (inExportHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 974aef8e8f..dec6cc5ef4 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -17,7 +17,7 @@ open Equality
type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t
(** To add rewriting rules to a base *)
-val add_rew_rules : string -> raw_rew_rule list -> unit
+val add_rew_rules : locality:Goptions.option_locality -> string -> raw_rew_rule list -> unit
(** The AutoRewrite tactic.
The optional conditions tell rewrite how to handle matching and side-condition solving.
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 39959d6fb8..167f7d4026 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -562,19 +562,18 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let open Context.Named.Declaration in
let open ReductionBehaviour in
let rec whrec cst_l (x, stack) =
- let () = if debug_RAKAM () then
+ let () = debug_RAKAM (fun () ->
let open Pp in
let pr c = Termops.Internal.print_constr_env env sigma c in
- Feedback.msg_debug
(h (str "<<" ++ pr x ++
str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
str "|" ++ cut () ++ Stack.pr pr stack ++
- str ">>"))
+ str ">>")))
in
let c0 = EConstr.kind sigma x in
let fold () =
- let () = if debug_RAKAM () then
- let open Pp in Feedback.msg_debug (str "<><><><><>") in
+ let () = debug_RAKAM (fun () ->
+ Pp.(str "<><><><><>")) in
((EConstr.of_kind c0, stack),cst_l)
in
match c0 with
@@ -820,3 +819,15 @@ let whd_cbn flags env sigma t =
(whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty))
in
Stack.zip ~refold:true sigma state
+
+let norm_cbn flags env sigma t =
+ let push_rel_check_zeta d env =
+ let open CClosure.RedFlags in
+ let d = match d with
+ | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
+ | d -> d in
+ push_rel d env in
+ let rec strongrec env t =
+ map_constr_with_full_binders env sigma
+ push_rel_check_zeta strongrec env (whd_cbn flags env sigma t) in
+ strongrec env t
diff --git a/tactics/cbn.mli b/tactics/cbn.mli
index af54771382..a02a74f9e4 100644
--- a/tactics/cbn.mli
+++ b/tactics/cbn.mli
@@ -8,6 +8,13 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+(** Weak-head cbn reduction. Despite the name, the cbn reduction is a complex
+ reduction distinct from call-by-name or call-by-need. *)
val whd_cbn :
CClosure.RedFlags.reds ->
Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
+
+(** Strong variant of cbn reduction. *)
+val norm_cbn :
+ CClosure.RedFlags.reds ->
+ Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9e66e8668f..d93501eea6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1014,10 +1014,11 @@ let deps_of_constraints cstrs evm p =
cstrs
let evar_dependencies pred evm p =
+ let cache = Evarutil.create_undefined_evars_cache () in
Evd.fold_undefined
(fun ev evi _ ->
if Evd.is_typeclass_evar evm ev && pred evm ev evi then
- let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+ let evars = Evar.Set.add ev (Evarutil.filtered_undefined_evars_of_evar_info ~cache evm evi)
in Intpart.union_set evars p
else ())
evm ()
diff --git a/tactics/dune b/tactics/dune
index 908dde5253..29378f52d1 100644
--- a/tactics/dune
+++ b/tactics/dune
@@ -1,6 +1,6 @@
(library
(name tactics)
(synopsis "Coq's Core Tactics [ML implementation]")
- (public_name coq.tactics)
+ (public_name coq-core.tactics)
(wrapped false)
(libraries printing))
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 9a55cabc86..9e7843b2bb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -19,7 +19,6 @@ open Tacmach.New
open Tacticals.New
open Clenv
open Tactics
-open Proofview.Notations
type branch_args = {
branchnum : int; (* the branch number *)
@@ -28,8 +27,6 @@ type branch_args = {
true=assumption, false=let-in *)
branchnames : Tactypes.intro_patterns}
-module NamedDecl = Context.Named.Declaration
-
type elim_kind = Case of bool | Elim
(* Find the right elimination suffix corresponding to the sort of the goal *)
@@ -217,52 +214,3 @@ let h_decompose l c = decompose_these c l
let h_decompose_or = decompose_or
let h_decompose_and = decompose_and
-
-(* The tactic Double performs a double induction *)
-
-let induction_trailer abs_i abs_j bargs =
- tclTHEN
- (tclDO (abs_j - abs_i) intro)
- (onLastHypId
- (fun id ->
- Proofview.Goal.enter begin fun gl ->
- let idty = pf_get_type_of gl (mkVar id) in
- let fvty = global_vars (pf_env gl) (project gl) idty in
- let possible_bring_hyps =
- (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs
- in
- let (hyps,_) =
- List.fold_left
- (fun (bring_ids,leave_ids) d ->
- let cid = NamedDecl.get_id d in
- if not (List.mem cid leave_ids)
- then (d::bring_ids,leave_ids)
- else (bring_ids,cid::leave_ids))
- ([],fvty) possible_bring_hyps
- in
- let ids = List.rev (ids_of_named_context hyps) in
- (tclTHENLIST
- [revert ids; elimination_then (fun _ -> tclIDTAC) id])
- end
- ))
-
-let double_ind h1 h2 =
- Proofview.Goal.enter begin fun gl ->
- let abs_i = depth_of_quantified_hypothesis true h1 gl in
- let abs_j = depth_of_quantified_hypothesis true h2 gl in
- let abs =
- if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
- if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else
- let info = Exninfo.reify () in
- tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in
- abs >>= fun (abs_i,abs_j) ->
- (tclTHEN (tclDO abs_i intro)
- (onLastHypId
- (fun id ->
- elimination_then
- (introElimAssumsThen (induction_trailer abs_i abs_j)) id)))
- end
-
-let h_double_induction = double_ind
-
-
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 01053502e4..a603b472f7 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -21,4 +21,3 @@ val case_tac : bool -> or_and_intro_pattern option ->
val h_decompose : inductive list -> constr -> unit Proofview.tactic
val h_decompose_or : constr -> unit Proofview.tactic
val h_decompose_and : constr -> unit Proofview.tactic
-val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0cc8becd8f..5e9c3baeb1 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1019,18 +1019,6 @@ let remove_hint dbname grs =
let db' = Hint_db.remove_list env grs db in
searchtable_add (dbname, db')
-type hint_action =
- | CreateDB of bool * TransparentState.t
- | AddTransparency of {
- superglobal : bool;
- grefs : evaluable_global_reference hints_transparency_target;
- state : bool;
- }
- | AddHints of { superglobal : bool; hints : hint_entry list }
- | RemoveHints of { superglobal : bool; hints : GlobRef.t list }
- | AddCut of { superglobal : bool; paths : hints_path }
- | AddMode of { superglobal : bool; gref : GlobRef.t; mode : hint_mode array }
-
let add_cut dbname path =
let db = get_db dbname in
let db' = Hint_db.add_cut path db in
@@ -1041,30 +1029,72 @@ let add_mode dbname l m =
let db' = Hint_db.add_mode l m db in
searchtable_add (dbname, db')
+type db_obj = {
+ db_local : bool;
+ db_name : string;
+ db_use_dn : bool;
+ db_ts : TransparentState.t;
+}
+
+let cache_db (_, {db_name=name; db_use_dn=b; db_ts=ts}) =
+ searchtable_add (name, Hint_db.empty ~name ts b)
+
+let load_db _ x = cache_db x
+
+let classify_db db = if db.db_local then Dispose else Substitute db
+
+let inDB : db_obj -> obj =
+ declare_object {(default_object "AUTOHINT_DB") with
+ cache_function = cache_db;
+ load_function = load_db;
+ subst_function = (fun (_,x) -> x);
+ classify_function = classify_db; }
+
+let create_hint_db l n ts b =
+ let hint = {db_local=l; db_name=n; db_use_dn=b; db_ts=ts} in
+ Lib.add_anonymous_leaf (inDB hint)
+
+type hint_action =
+ | AddTransparency of {
+ grefs : evaluable_global_reference hints_transparency_target;
+ state : bool;
+ }
+ | AddHints of hint_entry list
+ | RemoveHints of GlobRef.t list
+ | AddCut of hints_path
+ | AddMode of { gref : GlobRef.t; mode : hint_mode array }
+
+type hint_locality = Local | Export | SuperGlobal
+
type hint_obj = {
- hint_local : bool;
+ hint_local : hint_locality;
hint_name : string;
hint_action : hint_action;
}
+let superglobal h = match h.hint_local with
+ | SuperGlobal -> true
+ | Local | Export -> false
+
let load_autohint _ (kn, h) =
let name = h.hint_name in
+ let superglobal = superglobal h in
match h.hint_action with
- | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b)
- | AddTransparency { superglobal; grefs; state } ->
+ | AddTransparency { grefs; state } ->
if superglobal then add_transparency name grefs state
- | AddHints { superglobal; hints } ->
+ | AddHints hints ->
if superglobal then add_hint name hints
- | RemoveHints { superglobal; hints } ->
+ | RemoveHints hints ->
if superglobal then remove_hint name hints
- | AddCut { superglobal; paths } ->
+ | AddCut paths ->
if superglobal then add_cut name paths
- | AddMode { superglobal; gref; mode } ->
+ | AddMode { gref; mode } ->
if superglobal then add_mode name gref mode
let open_autohint i (kn, h) =
+ let superglobal = superglobal h in
if Int.equal i 1 then match h.hint_action with
- | AddHints { superglobal; hints } ->
+ | AddHints hints ->
let () =
if not superglobal then
(* Import-bound hints must be declared when not imported yet *)
@@ -1073,15 +1103,14 @@ let open_autohint i (kn, h) =
in
let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
List.iter add hints
- | AddCut { superglobal; paths } ->
+ | AddCut paths ->
if not superglobal then add_cut h.hint_name paths
- | AddTransparency { superglobal; grefs; state } ->
+ | AddTransparency { grefs; state } ->
if not superglobal then add_transparency h.hint_name grefs state
- | RemoveHints { superglobal; hints } ->
+ | RemoveHints hints ->
if not superglobal then remove_hint h.hint_name hints
- | AddMode { superglobal; gref; mode } ->
+ | AddMode { gref; mode } ->
if not superglobal then add_mode h.hint_name gref mode
- | CreateDB _ -> ()
let cache_autohint (kn, obj) =
load_autohint 1 (kn, obj); open_autohint 1 (kn, obj)
@@ -1137,8 +1166,7 @@ let subst_autohint (subst, obj) =
if k' == k && data' == data then hint else (k',data')
in
let action = match obj.hint_action with
- | CreateDB _ -> obj.hint_action
- | AddTransparency { superglobal; grefs = target; state = b } ->
+ | AddTransparency { grefs = target; state = b } ->
let target' =
match target with
| HintsVariables -> target
@@ -1148,26 +1176,28 @@ let subst_autohint (subst, obj) =
if grs == grs' then target
else HintsReferences grs'
in
- if target' == target then obj.hint_action else AddTransparency { superglobal; grefs = target'; state = b }
- | AddHints { superglobal; hints } ->
+ if target' == target then obj.hint_action else AddTransparency { grefs = target'; state = b }
+ | AddHints hints ->
let hints' = List.Smart.map subst_hint hints in
- if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' }
- | RemoveHints { superglobal; hints = grs } ->
+ if hints' == hints then obj.hint_action else AddHints hints'
+ | RemoveHints grs ->
let grs' = List.Smart.map (subst_global_reference subst) grs in
- if grs == grs' then obj.hint_action else RemoveHints { superglobal; hints = grs' }
- | AddCut { superglobal; paths = path } ->
+ if grs == grs' then obj.hint_action else RemoveHints grs'
+ | AddCut path ->
let path' = subst_hints_path subst path in
- if path' == path then obj.hint_action else AddCut { superglobal; paths = path' }
- | AddMode { superglobal; gref = l; mode = m } ->
+ if path' == path then obj.hint_action else AddCut path'
+ | AddMode { gref = l; mode = m } ->
let l' = subst_global_reference subst l in
- if l' == l then obj.hint_action else AddMode { superglobal; gref = l'; mode = m }
+ if l' == l then obj.hint_action else AddMode { gref = l'; mode = m }
in
if action == obj.hint_action then obj else { obj with hint_action = action }
let classify_autohint obj =
match obj.hint_action with
- | AddHints { hints = [] } -> Dispose
- | _ -> if obj.hint_local then Dispose else Substitute obj
+ | AddHints [] -> Dispose
+ | _ -> match obj.hint_local with
+ | Local -> Dispose
+ | Export | SuperGlobal -> Substitute obj
let inAutoHint : hint_obj -> obj =
declare_object {(default_object "AUTOHINT") with
@@ -1177,27 +1207,45 @@ let inAutoHint : hint_obj -> obj =
subst_function = subst_autohint;
classify_function = classify_autohint; }
-let make_hint ?(local = false) name action = {
+let make_hint ~local name action = {
hint_local = local;
hint_name = name;
hint_action = action;
}
-let create_hint_db l n st b =
- let hint = make_hint ~local:l n (CreateDB (b, st)) in
- Lib.add_anonymous_leaf (inAutoHint hint)
+let warn_deprecated_hint_without_locality =
+ CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
+ (fun () -> strbrk "The default value for hint locality is currently \
+ \"local\" in a section and \"global\" otherwise, but is scheduled to change \
+ in a future release. For the time being, adding hints outside of sections \
+ without specifying an explicit locality is therefore deprecated. It is \
+ recommended to use \"export\" whenever possible.")
+
+let check_hint_locality = let open Goptions in function
+| OptGlobal ->
+ if Global.sections_are_opened () then
+ CErrors.user_err Pp.(str
+ "This command does not support the global attribute in sections.");
+| OptExport ->
+ if Global.sections_are_opened () then
+ CErrors.user_err Pp.(str
+ "This command does not support the export attribute in sections.");
+| OptDefault ->
+ if not @@ Global.sections_are_opened () then
+ warn_deprecated_hint_without_locality ()
+| OptLocal -> ()
let interp_locality = function
-| Goptions.OptDefault | Goptions.OptGlobal -> false, true
-| Goptions.OptExport -> false, false
-| Goptions.OptLocal -> true, false
+| Goptions.OptDefault | Goptions.OptGlobal -> SuperGlobal
+| Goptions.OptExport -> Export
+| Goptions.OptLocal -> Local
let remove_hints ~locality dbnames grs =
- let local, superglobal = interp_locality locality in
+ let local = interp_locality locality in
let dbnames = if List.is_empty dbnames then ["core"] else dbnames in
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (RemoveHints { superglobal; hints = grs }) in
+ let hint = make_hint ~local dbname (RemoveHints grs) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1205,7 +1253,7 @@ let remove_hints ~locality dbnames grs =
(* The "Hint" vernacular command *)
(**************************************************************************)
-let add_resolves env sigma clist ~local ~superglobal dbnames =
+let add_resolves env sigma clist ~local dbnames =
List.iter
(fun dbname ->
let r =
@@ -1232,56 +1280,56 @@ let add_resolves env sigma clist ~local ~superglobal dbnames =
| _ -> ()
in
let () = if not !Flags.quiet then List.iter check r in
- let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in
+ let hint = make_hint ~local dbname (AddHints r) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_unfolds l ~local ~superglobal dbnames =
+let add_unfolds l ~local dbnames =
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (AddHints { superglobal; hints = List.map make_unfold l }) in
+ let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_cuts l ~local ~superglobal dbnames =
+let add_cuts l ~local dbnames =
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (AddCut { superglobal; paths = l }) in
+ let hint = make_hint ~local dbname (AddCut l) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_mode l m ~local ~superglobal dbnames =
+let add_mode l m ~local dbnames =
List.iter
(fun dbname ->
let m' = make_mode l m in
- let hint = make_hint ~local dbname (AddMode { superglobal; gref = l; mode = m' }) in
+ let hint = make_hint ~local dbname (AddMode { gref = l; mode = m' }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_transparency l b ~local ~superglobal dbnames =
+let add_transparency l b ~local dbnames =
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (AddTransparency { superglobal; grefs = l; state = b }) in
+ let hint = make_hint ~local dbname (AddTransparency { grefs = l; state = b }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_extern info tacast ~local ~superglobal dbname =
+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 { superglobal; hints = [make_extern (Option.get info.hint_priority) pat tacast] }) in
+ (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
Lib.add_anonymous_leaf (inAutoHint hint)
-let add_externs info tacast ~local ~superglobal dbnames =
- List.iter (add_extern info tacast ~local ~superglobal) dbnames
+let add_externs info tacast ~local dbnames =
+ List.iter (add_extern info tacast ~local) dbnames
-let add_trivials env sigma l ~local ~superglobal dbnames =
+let add_trivials env sigma l ~local dbnames =
List.iter
(fun dbname ->
let l = List.map (fun (name, c) -> make_trivial env sigma ~name c) l in
- let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in
+ let hint = make_hint ~local dbname (AddHints l) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1338,22 +1386,22 @@ let prepare_hint check env init (sigma,c) =
(c', diff)
let add_hints ~locality dbnames h =
- let local, superglobal = interp_locality locality in
+ let local = interp_locality locality in
if String.List.mem "nocore" dbnames then
user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
assert (not (List.is_empty dbnames));
let env = Global.env() in
let sigma = Evd.from_env env in
match h with
- | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames
- | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames
- | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames
- | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames
- | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames
+ | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local dbnames
+ | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local dbnames
+ | HintsCutEntry lhints -> add_cuts lhints ~local dbnames
+ | HintsModeEntry (l,m) -> add_mode l m ~local dbnames
+ | HintsUnfoldEntry lhints -> add_unfolds lhints ~local dbnames
| HintsTransparencyEntry (lhints, b) ->
- add_transparency lhints b ~local ~superglobal dbnames
+ add_transparency lhints b ~local dbnames
| HintsExternEntry (info, tacexp) ->
- add_externs info tacexp ~local ~superglobal dbnames
+ add_externs info tacexp ~local dbnames
let hint_globref gr = IsGlobRef gr
diff --git a/tactics/hints.mli b/tactics/hints.mli
index f5947bb946..381c7a1951 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -182,6 +182,8 @@ val searchtable_map : hint_db_name -> hint_db
val searchtable_add : (hint_db_name * hint_db) -> unit
+val check_hint_locality : Goptions.option_locality -> unit
+
(** [create_hint_db local name st use_dn].
[st] is a transparency state for unification using this db
[use_dn] switches the use of the discrimination net for all hints
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index b415b30de8..3ee85f6b1b 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -46,9 +46,6 @@ let cbv_native env sigma c =
let whd_cbn = Cbn.whd_cbn
-let strong_cbn flags =
- strong_with_flags whd_cbn flags
-
let simplIsCbn =
Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false
@@ -248,11 +245,11 @@ let reduction_of_red_expr_val = function
| Hnf -> (e_red hnf_constr,DEFAULTcast)
| Simpl (f,o) ->
let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in
- let am = if simplIsCbn () then strong_cbn f else simpl in
+ let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in
(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
| Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast)
| Cbn f ->
- (e_red (strong_cbn f), DEFAULTcast)
+ (e_red (Cbn.norm_cbn f), DEFAULTcast)
| Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast)
| Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
| Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
@@ -274,11 +271,14 @@ let reduction_of_red_expr env r =
let error_illegal_clause () =
CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.")
+let error_multiple_patterns () =
+ CErrors.user_err Pp.(str "\"at\" clause in occurences not supported with multiple patterns or references.")
+
let error_illegal_non_atomic_clause () =
CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.")
-let error_occurrences_not_unsupported () =
- CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.")
+let error_at_in_occurrences_not_supported () =
+ CErrors.user_err Pp.(str "\"at\" clause not supported for this reduction tactic.")
let bind_red_expr_occurrences occs nbcl redexp =
let open Locus in
@@ -295,14 +295,14 @@ let bind_red_expr_occurrences occs nbcl redexp =
else
match redexp with
| Unfold (_::_::_) ->
- error_illegal_clause ()
+ error_multiple_patterns ()
| Unfold [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Unfold [(occs,c)]
| Pattern (_::_::_) ->
- error_illegal_clause ()
+ error_multiple_patterns ()
| Pattern [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
@@ -325,7 +325,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
CbvNative (Some (occs,c))
| Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
| ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
- error_occurrences_not_unsupported ()
+ error_at_in_occurrences_not_supported ()
| Unfold [] | Pattern [] ->
assert false
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b40bdbc25e..67bf8d0d29 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -156,9 +156,6 @@ let convert_hyp ~check ~reorder d =
end
end
-let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
-
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
@@ -1244,8 +1241,6 @@ let force_destruction_arg with_evars env sigma c =
(* tactic "cut" (actually modus ponens) *)
(****************************************)
-let normalize_cut = false
-
let cut c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1260,8 +1255,6 @@ let cut c =
| sigma, s ->
let r = Sorts.relevance_of_sort s in
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
- (* Backward compat: normalize [c]. *)
- let c = if normalize_cut then strong whd_betaiota env sigma c else c in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun h ->
let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
@@ -1299,7 +1292,7 @@ let do_replace id = function
[Ti] and the first one (resp last one) being [G] whose hypothesis
[id] is replaced by P using the proof given by [tac] *)
-let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
+let clenv_refine_in ?err with_evars targetid replace sigma0 clenv tac =
let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in
let clenv = Clenv.update_clenv_evd clenv evd in
@@ -1310,11 +1303,10 @@ let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
let new_hyp_prf = clenv_value clenv in
let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
let naming = NamingMustBe (CAst.make targetid) in
- let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS (clear_metas evd))
(Tacticals.New.tclTHENLAST
- (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac)
+ (assert_after_then_gen ?err replace naming new_hyp_typ tac) exact_tac)
(********************************************)
(* Elimination tactics *)
@@ -1365,7 +1357,7 @@ let elimination_in_clause_scheme env sigma with_evars ~flags
if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
user_err ~hdr:"general_rewrite_in"
(str "Nothing to rewrite in " ++ Id.print id ++ str".");
- clenv_refine_in with_evars id id sigma elimclause''
+ clenv_refine_in with_evars id true sigma elimclause''
(fun id -> Proofview.tclUNIT ())
(*
@@ -1814,6 +1806,7 @@ let apply_in_once ?(respect_opaque = false) with_delta
let t' = Tacmach.New.pf_get_hyp_typ id gl in
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in
+ let replace = Id.equal id targetid in
let rec aux ?err idstoclear with_destruct c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1826,7 +1819,7 @@ let apply_in_once ?(respect_opaque = false) with_delta
if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
try
let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
- clenv_refine_in ?err with_evars targetid id sigma clause
+ clenv_refine_in ?err with_evars targetid replace sigma clause
(fun id ->
replace_error_option err (
apply_clear_request clear_flag false c <*>
@@ -2324,26 +2317,31 @@ let rewrite_hyp_then with_evars thin l2r id tac =
tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin))
end
-let prepare_naming ?loc = function
- | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id)
- | IntroAnonymous -> NamingAvoid Id.Set.empty
- | IntroFresh id -> NamingBasedOn (id, Id.Set.empty)
-
-let rec explicit_intro_names = let open CAst in function
-| {v=IntroForthcoming _} :: l -> explicit_intro_names l
-| {v=IntroNaming (IntroIdentifier id)} :: l -> Id.Set.add id (explicit_intro_names l)
+let rec collect_intro_names = let open CAst in function
+| {v=IntroForthcoming _} :: l -> collect_intro_names l
+| {v=IntroNaming (IntroIdentifier id)} :: l ->
+ let ids1, ids2 = collect_intro_names l in Id.Set.add id ids1, ids2
| {v=IntroAction (IntroOrAndPattern l)} :: l' ->
let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
- let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in
- List.fold_left fold Id.Set.empty ll
+ let fold (ids1',ids2') l =
+ let ids1, ids2 = collect_intro_names (l@l') in
+ Id.Set.union ids1 ids1', Id.Set.union ids2 ids2' in
+ List.fold_left fold (Id.Set.empty,Id.Set.empty) ll
| {v=IntroAction (IntroInjection l)} :: l' ->
- explicit_intro_names (l@l')
+ collect_intro_names (l@l')
| {v=IntroAction (IntroApplyOn (c,pat))} :: l' ->
- explicit_intro_names (pat::l')
-| {v=(IntroNaming (IntroAnonymous | IntroFresh _)
+ collect_intro_names (pat::l')
+| {v=IntroNaming (IntroFresh id)} :: l ->
+ let ids1, ids2 = collect_intro_names l in ids1, Id.Set.add id ids2
+| {v=(IntroNaming IntroAnonymous
| IntroAction (IntroWildcard | IntroRewrite _))} :: l ->
- explicit_intro_names l
-| [] -> Id.Set.empty
+ collect_intro_names l
+| [] -> Id.Set.empty, Id.Set.empty
+
+let explicit_intro_names l = fst (collect_intro_names l)
+
+let explicit_all_intro_names l =
+ let ids1,ids2 = collect_intro_names l in Id.Set.union ids1 ids2
let rec check_name_unicity env ok seen = let open CAst in function
| {v=IntroForthcoming _} :: l -> check_name_unicity env ok seen l
@@ -2368,30 +2366,33 @@ let rec check_name_unicity env ok seen = let open CAst in function
check_name_unicity env ok seen l
| [] -> ()
-let wild_id = Id.of_string "_tmp"
-
-let rec list_mem_assoc_right id = function
- | [] -> false
- | {CAst.v=id'}::l -> Id.equal id id' || list_mem_assoc_right id l
+let fresh_wild ids =
+ let rec aux s =
+ if Id.Set.exists (fun id -> String.is_prefix s (Id.to_string id)) ids
+ then aux (s ^ "'")
+ else Id.of_string s in
+ aux "_H"
-let check_thin_clash_then id thin avoid tac =
- if list_mem_assoc_right id thin then
- let newid = next_ident_away (add_suffix id "'") avoid in
- let thin =
- List.map CAst.(map (fun id' -> if Id.equal id id' then newid else id')) thin in
- Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin)
- else
- tac thin
+let make_naming ?loc avoid l = function
+ | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id)
+ | IntroAnonymous -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l))
+ | IntroFresh id -> NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))
-let make_tmp_naming avoid l = function
+let rec make_naming_action avoid l = function
(* In theory, we could use a tmp id like "wild_id" for all actions
but we prefer to avoid it to avoid this kind of "ugly" names *)
- (* Alternatively, we could have called check_thin_clash_then on
- IntroAnonymous, but at the cost of a "renaming"; Note that in the
- case of IntroFresh, we should use check_thin_clash_then anyway to
- prevent the case of an IntroFresh precisely using the wild_id *)
- | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l))
- | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l)))
+ | IntroWildcard ->
+ NamingBasedOn (fresh_wild (Id.Set.union avoid (explicit_all_intro_names l)), Id.Set.empty)
+ | IntroApplyOn (_,{CAst.v=pat;loc}) -> make_naming_pattern avoid ?loc l pat
+ | (IntroOrAndPattern _ | IntroInjection _ | IntroRewrite _) as pat ->
+ NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l)))
+
+and make_naming_pattern ?loc avoid l = function
+ | IntroNaming pat -> make_naming ?loc avoid l pat
+ | IntroAction pat -> make_naming_action avoid l pat
+ | IntroForthcoming _ -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l))
+
+let prepare_naming ?loc pat = make_naming ?loc Id.Set.empty [] pat
let fit_bound n = function
| None -> true
@@ -2430,38 +2431,21 @@ let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac =
[CAst.make @@ IntroNaming IntroAnonymous]
| {CAst.loc;v=pat} :: l ->
if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
+ let naming = make_naming_pattern avoid l pat in
match pat with
| IntroForthcoming onlydeps ->
- intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
- destopt onlydeps bound n
+ intro_forthcoming_then_gen naming destopt onlydeps bound n
(fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound
(n+List.length ids) tac l)
| IntroAction pat ->
- intro_then_gen (make_tmp_naming avoid l pat)
- destopt true false
+ intro_then_gen naming destopt true false
(intro_pattern_action ?loc with_evars pat thin destopt
(fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0
(fun ids thin ->
intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l)))
| IntroNaming pat ->
- intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l
-
- (* Pi-introduction rule, used backwards *)
-and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l =
- match pat with
- | IntroIdentifier id ->
- check_thin_clash_then id thin avoid (fun thin ->
- intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false
- (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l))
- | IntroAnonymous ->
- intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
- destopt true false
- (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)
- | IntroFresh id ->
- (* todo: avoid thinned names to interfere with generation of fresh name *)
- intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l)))
- destopt true false
- (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)
+ intro_then_gen naming destopt true false
+ (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound (n+1) tac l)
and intro_pattern_action ?loc with_evars pat thin destopt tac id =
match pat with
@@ -2474,24 +2458,16 @@ and intro_pattern_action ?loc with_evars pat thin destopt tac id =
| IntroRewrite l2r ->
rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None [])
| IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) ->
- let naming,tac_ipat =
- prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in
- let doclear =
- if naming = NamingMustBe (CAst.make ?loc id) then
- Proofview.tclUNIT () (* apply_in_once do a replacement *)
- else
- clear [id] in
- let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings))
- in
+ let naming = NamingMustBe (CAst.make ?loc id) in
+ let tac_ipat = prepare_action ?loc with_evars destopt pat in
+ let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in
apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f)
- (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
+ (fun id -> Tacticals.New.tclTHENLIST [tac_ipat id; tac thin None []])
-and prepare_intros ?loc with_evars dft destopt = function
+and prepare_action ?loc with_evars destopt = function
| IntroNaming ipat ->
- prepare_naming ?loc ipat,
- (fun id -> move_hyp id destopt)
+ (fun _ -> Proofview.tclUNIT ())
| IntroAction ipat ->
- prepare_naming ?loc dft,
(let tac thin bound =
intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0
(fun _ l -> clear_wildcards l) in
@@ -2528,9 +2504,19 @@ let intros_patterns with_evars = function
(* Forward reasoning *)
(**************************)
-let prepare_intros_opt with_evars dft destopt = function
- | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ())
- | Some {CAst.loc;v=ipat} -> prepare_intros ?loc with_evars dft destopt ipat
+let prepare_intros_opt with_evars dft destopt ipat =
+ let naming, loc, ipat = match ipat with
+ | None ->
+ let pat = IntroNaming dft in make_naming_pattern Id.Set.empty [] pat, None, pat
+ | Some {CAst.loc;v=(IntroNaming pat as ipat)} ->
+ (* "apply ... in H as id" needs to use id and H is kept iff id<>H *)
+ prepare_naming ?loc pat, loc, ipat
+ | Some {CAst.loc;v=(IntroAction pat as ipat)} ->
+ (* "apply ... in H as pat" reuses H so that old H is always cleared *)
+ (match dft with IntroIdentifier _ -> prepare_naming ?loc dft | _ -> make_naming_action Id.Set.empty [] pat),
+ loc, ipat
+ | Some {CAst.loc;v=(IntroForthcoming _)} -> assert false in
+ naming, prepare_action ?loc with_evars destopt ipat
let ipat_of_name = function
| Anonymous -> None
@@ -2810,7 +2796,24 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
let open Context.Rel.Declaration in
let decls,cl = decompose_prod_n_assum sigma i cl in
let dummy_prod = it_mkProd_or_LetIn mkProp decls in
- let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
+ let newdecls,_ =
+ let c = Termops.collapse_appl sigma c in
+ let arity = Array.length (snd (Termops.decompose_app_vect sigma c)) in
+ let cache = ref Int.Map.empty in
+ let eq sigma k t =
+ let c =
+ try Int.Map.find k !cache
+ with Not_found ->
+ let c = EConstr.Vars.lift k c in
+ let () = cache := Int.Map.add k c !cache in
+ c
+ in
+ (* We use a nounivs equality because generalize morally takes a pattern as
+ argument, so we have to ignore freshly generated sorts. *)
+ EConstr.eq_constr_nounivs sigma c t
+ in
+ decompose_prod_n_assum sigma i (replace_term_gen sigma eq arity (mkRel 1) dummy_prod)
+ in
let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
let na = generalized_name env sigma c t ids cl' na in
let r = Retyping.relevance_of_type env sigma t in
@@ -3045,8 +3048,7 @@ let specialize (c,lbind) ipat =
match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with
| Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) ->
(* Like assert (id:=id args) but with the concept of specialization *)
- let naming,tac =
- prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in
+ let naming,tac = prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in
let repl = do_replace (Some id) naming in
Tacticals.New.tclTHENFIRST
(assert_before_then_gen repl naming typ tac)
@@ -3059,10 +3061,10 @@ let specialize (c,lbind) ipat =
(* TODO: add intro to be more homogeneous. It will break
scripts but will be easy to fix *)
(Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term))
- | Some {CAst.loc;v=ipat} ->
+ | Some _ as ipat ->
(* Like pose proof with extra support for "with" bindings *)
(* even though the "with" bindings forces full application *)
- let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in
+ let naming, tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in
Tacticals.New.tclTHENFIRST
(assert_before_then_gen false naming typ tac)
(exact_no_check term)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a6471be549..c07073a91a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -35,10 +35,6 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
val introduction : Id.t -> unit Proofview.tactic
val convert_concl : check:bool -> types -> cast_kind -> unit Proofview.tactic
val convert_hyp : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
-val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_concl]"]
-val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_hyp]"]
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
val fix : Id.t -> int -> unit Proofview.tactic
@@ -81,11 +77,6 @@ val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic
val intros : unit Proofview.tactic
-(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
- the conclusion of goal [g], up to head-reduction if [b] is [true] *)
-val depth_of_quantified_hypothesis :
- bool -> quantified_hypothesis -> Proofview.Goal.t -> int
-
val intros_until : quantified_hypothesis -> unit Proofview.tactic
val intros_clearing : bool list -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 23:17:34 +0000