aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli4
-rw-r--r--plugins/ssr/ssrcommon.ml19
-rw-r--r--plugins/ssr/ssrelim.ml3
-rw-r--r--plugins/ssr/ssrfwd.ml3
-rw-r--r--plugins/ssr/ssripats.ml69
-rw-r--r--plugins/ssr/ssrparser.ml465
-rw-r--r--plugins/ssr/ssrparser.mli4
-rw-r--r--plugins/ssr/ssrprinters.ml3
-rw-r--r--plugins/ssr/ssrtacticals.ml10
-rw-r--r--plugins/ssr/ssrtacticals.mli4
-rw-r--r--plugins/ssr/ssrvernac.ml424
-rw-r--r--plugins/ssr/ssrview.ml93
-rw-r--r--plugins/ssr/ssrview.mli6
13 files changed, 178 insertions, 129 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 7f5f2f63d7..6ba937a2ff 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option
(* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
-type ssrindex = int Misctypes.or_var
+type ssrindex = int Locus.or_var
(* clear switch {H G} *)
type ssrclear = ssrhyps
@@ -88,7 +88,7 @@ type ssripat =
| IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *)
| IPatInj of ssripatss
| IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir
- | IPatView of ssrview (* /view *)
+ | IPatView of bool * ssrview (* {}/view (true if the clear is present) *)
| IPatClear of ssrclear (* {H1 H2} *)
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Id.t list
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c0026616d3..54f3f9c718 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,10 +181,9 @@ let option_assert_get o msg =
(** Constructors for rawconstr *)
open Glob_term
open Globnames
-open Misctypes
open Decl_kinds
-let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
+let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
let rec isRHoles cl = match cl with
@@ -254,7 +253,7 @@ let interp_refine ist gl rc =
let interp_open_constr ist gl gc =
- let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in
+ let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in
(project gl, (sigma, c))
let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
@@ -423,12 +422,12 @@ let mk_anon_id t gl_ids =
(set s i (Char.chr (Char.code (get s i) + 1)); s) in
Id.of_bytes (loop (n - 1))
-let convert_concl_no_check t = Tactics.convert_concl_no_check t Term.DEFAULTcast
-let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast
+let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast
+let convert_concl t = Tactics.convert_concl t DEFAULTcast
let rename_hd_prod orig_name_ref gl =
match EConstr.kind (project gl) (pf_concl gl) with
- | Term.Prod(_,src,tgt) ->
+ | Prod(_,src,tgt) ->
Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl
| _ -> CErrors.anomaly (str "gentac creates no product")
@@ -859,10 +858,10 @@ open Util
(** Constructors for constr_expr *)
let mkCProp loc = CAst.make ?loc @@ CSort GProp
let mkCType loc = CAst.make ?loc @@ CSort (GType [])
-let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None)
+let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)
let rec mkCHoles ?loc n =
- if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
-let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
+ if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
+let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)
let mkCLambda ?loc name ty t = CAst.make ?loc @@
CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
let mkCArrow ?loc ty t = CAst.make ?loc @@
@@ -1446,7 +1445,7 @@ let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return
let tclRENAME_HD_PROD name = Goal.enter begin fun gl ->
let convert_concl_no_check t =
- Tactics.convert_concl_no_check t Term.DEFAULTcast in
+ Tactics.convert_concl_no_check t DEFAULTcast in
let concl = Goal.concl gl in
let sigma = Goal.sigma gl in
match EConstr.kind sigma concl with
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 87d107d651..fbe3b000fb 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -14,9 +14,10 @@ open Util
open Names
open Printer
open Term
+open Constr
open Termops
open Globnames
-open Misctypes
+open Tactypes
open Tacmach
open Ssrmatching_plugin
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index c6beb08c5e..7fe2421f90 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
let cl = EConstr.Unsafe.to_constr cl in
try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in
+ let gl = pf_merge_uc ucst gl in
let c = EConstr.of_constr c in
let cl = EConstr.of_constr cl in
if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++
@@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
| Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
| _ -> c, pfe_type_of gl c in
let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in
- let gl = pf_merge_uc ucst gl in
Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl
open Util
@@ -86,7 +86,6 @@ let _ =
open Constrexpr
open Glob_term
-open Misctypes
let combineCG t1 t2 f g = match t1, t2 with
| (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index b397c55315..46fde41150 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -12,6 +12,7 @@ open Ssrmatching_plugin
open Util
open Names
+open Constr
open Proofview
open Proofview.Notations
@@ -90,11 +91,11 @@ open State
(** Warning: unlike [nb_deps_assums], it does not perform reduction *)
let rec nb_assums cur env sigma t =
match EConstr.kind sigma t with
- | Term.Prod(name,ty,body) ->
+ | Prod(name,ty,body) ->
nb_assums (cur+1) env sigma body
- | Term.LetIn(name,ty,t1,t2) ->
+ | LetIn(name,ty,t1,t2) ->
nb_assums (cur+1) env sigma t2
- | Term.Cast(t,_,_) ->
+ | Cast(t,_,_) ->
nb_assums cur env sigma t
| _ -> cur
let nb_assums = nb_assums 0
@@ -118,13 +119,10 @@ let intro_end =
Ssrcommon.tcl0G (isCLR_CONSUME)
(** [=> _] *****************************************************************)
-let intro_clear ids future_ipats =
+let intro_clear ids =
Goal.enter begin fun gl ->
let _, clear_ids, ren =
List.fold_left (fun (used_ids, clear_ids, ren) id ->
- if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin
- used_ids, id :: clear_ids, ren
- end else
let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in
(new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren))
(Tacmach.New.pf_ids_of_hyps gl, [], []) ids
@@ -212,22 +210,22 @@ let tclLOG p t =
tclUNIT ()
end
-let rec ipat_tac1 future_ipats ipat : unit tactic =
+let rec ipat_tac1 ipat : unit tactic =
match ipat with
- | IPatView l ->
- Ssrview.tclIPAT_VIEWS ~views:l
- ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats)
+ | IPatView (clear_if_id,l) ->
+ Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id
+ ~conclusion:(fun ~to_clear:clr -> intro_clear clr)
| IPatDispatch ipatss ->
- tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) []
+ tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
| IPatId id -> Ssrcommon.tclINTRO_ID id
| IPatCase ipatss ->
- tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss
+ tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
| IPatInj ipatss ->
tclIORPAT (Ssrcommon.tclWITHTOP
(fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t)))
- future_ipats ipatss
+ ipatss
| IPatAnon Drop -> intro_drop
| IPatAnon One -> Ssrcommon.tclINTRO_ANON
@@ -238,7 +236,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatClear ids ->
tacCHECK_HYPS_EXIST ids <*>
- intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+ intro_clear (List.map Ssrcommon.hyp_id ids)
| IPatSimpl (Simpl n) ->
V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
@@ -255,17 +253,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatTac t -> t
-and ipat_tac future_ipats pl : unit tactic =
+and ipat_tac pl : unit tactic =
match pl with
| [] -> tclUNIT ()
| pat :: pl ->
- Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*>
+ Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*>
isTICK pat <*>
- ipat_tac future_ipats pl
+ ipat_tac pl
-and tclIORPAT tac future_ipats = function
+and tclIORPAT tac = function
| [[]] -> tac
- | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p)
+ | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p)
let split_at_first_case ipats =
let rec loop acc = function
@@ -281,12 +279,27 @@ let ssr_exception is_on = function
let option_to_list = function None -> [] | Some x -> [x]
+(* Simple pass doing {x}/v -> /v{x} *)
+let elaborate_ipats l =
+ let rec elab = function
+ | [] -> []
+ | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest
+ | IPatDispatch p :: rest -> IPatDispatch (List.map elab p) :: elab rest
+ | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest
+ | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest
+ | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ |
+ IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ |
+ IPatAbstractVars _) as x :: rest -> x :: elab rest
+ in
+ elab l
+
let main ?eqtac ~first_case_is_dispatch ipats =
+ let ipats = elaborate_ipats ipats in
let ip_before, case, ip_after = split_at_first_case ipats in
let case = ssr_exception first_case_is_dispatch case in
let case = option_to_list case in
let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in
- Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
+ Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
end (* }}} *)
@@ -556,7 +569,7 @@ let rec eqmoveipats eqpat = function
let ssrsmovetac = Goal.enter begin fun g ->
let sigma, concl = Goal.(sigma g, concl g) in
match EConstr.kind sigma concl with
- | Term.Prod _ | Term.LetIn _ -> tclUNIT ()
+ | Prod _ | LetIn _ -> tclUNIT ()
| _ -> Tactics.hnf_in_concl
end
@@ -575,7 +588,7 @@ let ssrmovetac = function
(tacVIEW_THEN_GRAB view ~conclusion) <*>
tclIPAT (IPatClear clr :: ipats)
| _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
- tclIPAT (IPatView view :: IPatClear clr :: ipats)
+ tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats)
| _, (Some pat, (dgens, ipats)) ->
let dgentac = with_dgens dgens eqmovetac in
dgentac <*> tclIPAT (eqmoveipats pat ipats)
@@ -594,8 +607,8 @@ let rec is_Evar_or_CastedMeta sigma x =
let occur_existential_or_casted_meta sigma c =
let rec occrec c = match EConstr.kind sigma c with
- | Term.Evar _ -> raise Not_found
- | Term.Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
+ | Evar _ -> raise Not_found
+ | Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
| _ -> EConstr.iter sigma occrec c
in
try occrec c; false
@@ -625,7 +638,7 @@ let tacFIND_ABSTRACT_PROOF check_lock abstract_n =
let sigma, env = Goal.(sigma g, env g) in
let l = Evd.fold_undefined (fun e ei l ->
match EConstr.kind sigma ei.Evd.evar_concl with
- | Term.App(hd, [|ty; n; lock|])
+ | App(hd, [|ty; n; lock|])
when (not check_lock ||
(occur_existential_or_casted_meta sigma ty &&
is_Evar_or_CastedMeta sigma lock)) &&
@@ -654,8 +667,8 @@ let ssrabstract dgens =
let sigma, env, concl = Goal.(sigma g, env g, concl g) in
let t = args_id.(0) in
match EConstr.kind sigma t with
- | (Term.Evar _ | Term.Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
- | Term.Cast(m,_,_)
+ | (Evar _ | Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
+ | Cast(m,_,_)
when EConstr.isEvar sigma m || EConstr.isMeta sigma m ->
Ssrcommon.tacUNIFY concl t <*> tclUNIT id
| _ ->
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 5f39674407..347a1e4e26 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -10,6 +10,7 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+let _vmcast = Constr.VMcast
open Names
open Pp
open Pcoq
@@ -17,18 +18,19 @@ open Ltac_plugin
open Genarg
open Stdarg
open Tacarg
-open Term
open Libnames
open Tactics
open Tacmach
open Util
+open Locus
open Tacexpr
open Tacinterp
open Pltac
open Extraargs
open Ppconstr
-open Misctypes
+open Namegen
+open Tactypes
open Decl_kinds
open Constrexpr
open Constrexpr_ops
@@ -64,7 +66,7 @@ DECLARE PLUGIN "ssreflect_plugin"
* we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = CLexer.get_keyword_state () ;;
-let tacltop = (5,Notation_term.E)
+let tacltop = (5,Notation_gram.E)
let pr_ssrtacarg _ _ prt = prt tacltop
ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
@@ -301,24 +303,24 @@ END
let pr_index = function
- | Misctypes.ArgVar {CAst.v=id} -> pr_id id
- | Misctypes.ArgArg n when n > 0 -> int n
+ | ArgVar {CAst.v=id} -> pr_id id
+ | ArgArg n when n > 0 -> int n
| _ -> mt ()
let pr_ssrindex _ _ _ = pr_index
-let noindex = Misctypes.ArgArg 0
+let noindex = ArgArg 0
let check_index ?loc i =
if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
let mk_index ?loc = function
- | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i)
+ | ArgArg i -> ArgArg (check_index ?loc i)
| iv -> iv
let interp_index ist gl idx =
Tacmach.project gl,
match idx with
- | Misctypes.ArgArg _ -> idx
- | Misctypes.ArgVar id ->
+ | ArgArg _ -> idx
+ | ArgVar id ->
let i =
try
let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
@@ -336,7 +338,7 @@ let interp_index ist gl idx =
| None -> raise Not_found
end end
with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
- Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
+ ArgArg (check_index ?loc:id.CAst.loc i)
open Pltac
@@ -410,8 +412,8 @@ let pr_docc = function
let pr_ssrdocc _ _ _ = pr_docc
ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc
-| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
| [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ]
+| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
END
(* Old kinds of terms *)
@@ -543,7 +545,7 @@ END
let remove_loc x = x.CAst.v
-let ipat_of_intro_pattern p = Misctypes.(
+let ipat_of_intro_pattern p = Tactypes.(
let rec ipat_of_intro_pattern = function
| IntroNaming (IntroIdentifier id) -> IPatId id
| IntroAction IntroWildcard -> IPatAnon Drop
@@ -576,7 +578,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
| IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
| IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
| IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
- | IPatView v -> IPatView (List.map map_ast_closure_term v)
+ | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v)
| IPatTac _ -> assert false (*internal usage only *)
let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
@@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist)
let interp_intro_pattern = interp_wit wit_intro_pattern
-let interp_introid ist gl id = Misctypes.(
+let interp_introid ist gl id =
try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id))))))
with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v
-)
let get_intro_id = function
| IntroNaming (IntroIdentifier id) -> id
| _ -> assert false
-let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
+let rec add_intro_pattern_hyps ipat hyps =
let {CAst.loc=loc;v=ipat} = ipat in
match ipat with
| IntroNaming (IntroIdentifier id) ->
@@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
| IntroForthcoming _ ->
(* As in ipat_of_intro_pattern, was unable to determine which kind
of ipat interp_introid could return [HH] *) assert false
-)
(* We interp the ipat using the standard ltac machinery for ids, since
* we have no clue what a name could be bound to (maybe another ipat) *)
@@ -646,7 +646,7 @@ let interp_ipat ist gl =
| IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat)
| IPatAbstractVars l ->
IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l))
- | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist
+ | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist
gl x)) l)
| (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x
| IPatTac _ -> assert false (*internal usage only *)
@@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
(* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *)
| [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ]
| [ ssrdocc(occ) "->" ] -> [ match occ with
+ | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
| None, occ -> [IPatRewrite (occ, L2R)]
| Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]]
| [ ssrdocc(occ) "<-" ] -> [ match occ with
+ | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
| None, occ -> [IPatRewrite (occ, R2L)]
| Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]]
+ | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with
+ | Some [], _ -> [IPatView (true,v)]
+ | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)]
+ | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ]
| [ ssrdocc(occ) ] -> [ match occ with
| Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl]
| _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")]
@@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
| [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ]
| [ "-/" integer(n) "/" integer (m) "=" ] ->
[ [IPatNoop;IPatSimpl(SimplCut(n,m))] ]
- | [ ssrfwdview(v) ] -> [ [IPatView v] ]
+ | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ]
| [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
| [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
END
@@ -1064,7 +1070,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
| BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
let bs, c' = format_constr_expr h c in
Bdef (x, oty, v) :: bs, c'
- | [BFcast], { v = CCast (c, CastConv t) } ->
+ | [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
[Bcast t], c
| BFrec (has_str, has_cast) :: h,
{ v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
@@ -1093,7 +1099,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
let mkFwdVal fk c = ((fk, []), c)
let mkssrFwdVal fk c = ((fk, []), (c,None))
-let dC t = CastConv t
+let dC t = Glob_term.CastConv t
let same_ist { interp_env = x } { interp_env = y } =
match x,y with
@@ -1154,7 +1160,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
END
let bvar_lname = let open CAst in function
- | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id
+ | { v = CRef (qid, _) } when qualid_is_ident qid ->
+ CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid)
| { loc = loc } -> CAst.make ?loc Anonymous
let pr_ssrbinder prc _ _ (_, c) = prc c
@@ -1210,8 +1217,8 @@ let push_binders c2 bs =
| [] -> c
| _ -> anomaly "binder not a lambda nor a let in" in
match c2 with
- | { loc; v = CCast (ct, CastConv cty) } ->
- CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs)))
+ | { loc; v = CCast (ct, Glob_term.CastConv cty) } ->
+ CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs)))
| ct -> loop false ct bs
let rec fix_binders = let open CAst in function
@@ -1246,7 +1253,8 @@ END
let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
let bvar_locid = function
- | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id
+ | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+ CAst.make ?loc:qid.CAst.loc (qualid_basename qid)
| _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")
@@ -1676,7 +1684,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt
let pr_ssrgen _ _ _ = pr_gen
ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen
-| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ]
+| [ ssrdocc(docc) cpattern(dt) ] -> [
+ match docc with
+ | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here")
+ | _ -> docc, dt ]
| [ cpattern(dt) ] -> [ nodocc, dt ]
END
@@ -1938,7 +1949,7 @@ END
let vmexacttac pf =
Goal.nf_enter begin fun gl ->
- exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl))
+ exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
end
TACTIC EXTEND ssrexact
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 2ac7c7e264..7cd3751cef 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -14,11 +14,11 @@ open Ltac_plugin
val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 11369228cb..8f4b2179e1 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -107,7 +107,8 @@ let rec pr_ipat p =
| IPatAnon All -> str "*"
| IPatAnon Drop -> str "_"
| IPatAnon One -> str "?"
- | IPatView v -> pr_view2 v
+ | IPatView (false,v) -> pr_view2 v
+ | IPatView (true,v) -> str"{}" ++ pr_view2 v
| IPatNoop -> str "-"
| IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
| IPatTac _ -> str "<tac>"
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 937e68b065..83581f3416 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -11,9 +11,9 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Names
+open Constr
open Termops
open Tacmach
-open Misctypes
open Locusops
open Ssrast
@@ -24,7 +24,7 @@ module NamedDecl = Context.Named.Declaration
(** Tacticals (+, -, *, done, by, do, =>, first, and last). *)
-let get_index = function ArgArg i -> i | _ ->
+let get_index = function Locus.ArgArg i -> i | _ ->
anomaly "Uninterpreted index"
(* Toplevel constr must be globalized twice ! *)
@@ -103,10 +103,10 @@ let endclausestac id_map clseq gl_id cl0 gl =
| ids, dc' ->
forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in
let rec unmark c = match EConstr.kind (project gl) c with
- | Term.Var id when hidden_clseq clseq && id = gl_id -> cl0
- | Term.Prod (Name id, t, c') when List.mem_assoc id id_map ->
+ | Var id when hidden_clseq clseq && id = gl_id -> cl0
+ | Prod (Name id, t, c') when List.mem_assoc id id_map ->
EConstr.mkProd (Name (orig_id id), unmark t, unmark c')
- | Term.LetIn (Name id, v, t, c') when List.mem_assoc id id_map ->
+ | LetIn (Name id, v, t, c') when List.mem_assoc id id_map ->
EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c')
| _ -> EConstr.map (project gl) unmark c in
let utac hyp =
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index a5636ad0f0..684e002352 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -17,7 +17,7 @@ val tclSEQAT :
Tacinterp.interp_sign ->
Tacinterp.Value.t ->
Ssrast.ssrdir ->
- int Misctypes.or_var *
+ int Locus.or_var *
(('a * Tacinterp.Value.t option list) *
Tacinterp.Value.t option) ->
Tacmach.tactic
@@ -37,7 +37,7 @@ val hinttac :
val ssrdotac :
Tacinterp.interp_sign ->
- ((int Misctypes.or_var * Ssrast.ssrmmod) *
+ ((int Locus.or_var * Ssrast.ssrmmod) *
(bool * Tacinterp.Value.t option list)) *
((Ssrast.ssrhyps *
((Ssrast.ssrhyp_or_id * string) *
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 05dbf0a86d..7ce2dd64af 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -19,7 +19,7 @@ open Constrexpr_ops
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Vernac_
+open Pvernac.Vernac_
open Ltac_plugin
open Notation_ops
open Notation_term
@@ -27,9 +27,7 @@ open Glob_term
open Globnames
open Stdarg
open Genarg
-open Misctypes
open Decl_kinds
-open Libnames
open Pp
open Ppconstr
open Printer
@@ -144,21 +142,21 @@ END
let declare_one_prenex_implicit locality f =
let fref =
try Smartlocate.global_with_alias f
- with _ -> errorstrm (pr_reference f ++ str " is not declared") in
+ with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
let rec loop = function
| a :: args' when Impargs.is_status_implicit a ->
(ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args'
| args' when List.exists Impargs.is_status_implicit args' ->
- errorstrm (str "Expected prenex implicits for " ++ pr_reference f)
+ errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
| _ -> [] in
let impls =
match Impargs.implicits_of_global fref with
| [cond,impls] -> impls
- | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f)
+ | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f)
| _ -> errorstrm (str "Multiple implicits not supported") in
match loop impls with
| [] ->
- errorstrm (str "Expected some implicits for " ++ pr_reference f)
+ errorstrm (str "Expected some implicits for " ++ pr_qualid f)
| impls ->
Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
@@ -377,7 +375,10 @@ let interp_head_pat hpat =
| Cast (c', _, _) -> loop c'
| Prod (_, _, c') -> loop c'
| LetIn (_, _, _, c') -> loop c'
- | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in
+ | _ ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
filter_head, loop
let all_true _ = true
@@ -413,7 +414,7 @@ let interp_search_arg arg =
(* Module path postfilter *)
-let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m
+let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m
let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc
@@ -431,10 +432,9 @@ GEXTEND Gram
END
let interp_modloc mr =
- let interp_mod (_, mr) =
- let {CAst.loc=loc; v=qid} = qualid_of_reference mr in
+ let interp_mod (_, qid) =
try Nametab.full_name_module qid with Not_found ->
- CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in
+ CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in
let mr_out, mr_in = List.partition fst mr in
let interp_bmod b = function
| [] -> fun _ _ _ -> true
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 29a936381f..3f974ea063 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -67,9 +67,9 @@ end
module State : sig
(* View storage API *)
- val vsINIT : EConstr.t -> unit tactic
- val vsPUSH : (EConstr.t -> EConstr.t tactic) -> unit tactic
- val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic
+ val vsINIT : EConstr.t * Id.t list -> unit tactic
+ val vsPUSH : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic
+ val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic
val vsASSERT_EMPTY : unit tactic
end = struct (* {{{ *)
@@ -78,6 +78,7 @@ type vstate = {
subject_name : Id.t option; (* top *)
(* None if views are being applied to a term *)
view : EConstr.t; (* v2 (v1 top) *)
+ to_clear : Id.t list;
}
include Ssrcommon.MakeState(struct
@@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct
let init = None
end)
-let vsINIT view = tclSET (Some { subject_name = None; view })
+let vsINIT (view, to_clear) =
+ tclSET (Some { subject_name = None; view; to_clear })
let vsPUSH k =
tacUPDATE (fun s -> match s with
- | Some { subject_name; view } ->
- k view >>= fun view ->
- tclUNIT (Some { subject_name; view })
+ | Some { subject_name; view; to_clear } ->
+ k view >>= fun (view, clr) ->
+ tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr })
| None ->
Goal.enter_one ~__LOC__ begin fun gl ->
let concl = Goal.concl gl in
@@ -102,15 +104,15 @@ let vsPUSH k =
| _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in
let view = EConstr.mkVar id in
Ssrcommon.tclINTRO_ID id <*>
- k view >>= fun view ->
- tclUNIT (Some { subject_name = Some id; view })
+ k view >>= fun (view, to_clear) ->
+ tclUNIT (Some { subject_name = Some id; view; to_clear })
end)
let vsCONSUME k =
tclGET (fun s -> match s with
- | Some { subject_name; view } ->
+ | Some { subject_name; view; to_clear } ->
tclSET None <*>
- k subject_name view
+ k ~name:subject_name view ~to_clear
| None -> anomaly "vsCONSUME: empty storage")
let vsASSERT_EMPTY =
@@ -157,7 +159,7 @@ let tclINJ_CONSTR_IST ist p =
let mkGHole =
DAst.make
- (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+ (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None))
let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
let mkGApp f args =
if args = [] then f
@@ -187,6 +189,16 @@ end
* modular, see the 2 functions below that would need to "uncommit" *)
let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
+let tclADD_CLEAR_IF_ID (env, ist, t) x =
+ Ssrprinters.ppdebug (lazy
+ Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t));
+ let hd, _ = EConstr.decompose_app ist t in
+ match EConstr.kind ist hd with
+ | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id])
+ | _ -> tclUNIT (x,[])
+
+let tclPAIR p x = tclUNIT (x, p)
+
(* The ssr heuristic : *)
(* Estimate a bound on the number of arguments of a raw constr. *)
(* This is not perfect, because the unifier may fail to *)
@@ -203,14 +215,15 @@ let guess_max_implicits ist glob =
(fun _ -> tclUNIT 5)
let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
- interp_glob ist glob >>= fun (env, sigma, term) ->
+ interp_glob ist glob >>= fun (env, sigma, term as ot) ->
let term_ty = Retyping.get_type_of env sigma term in
let ctx, i = Reductionops.splay_prod env sigma term_ty in
let rel_ctx =
List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in
- if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i
- then tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
- else Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+ if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i)
+ then Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+ else tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
+ >>= tclADD_CLEAR_IF_ID ot
end
(* There are two ways of "applying" a view to term: *)
@@ -221,7 +234,7 @@ end
(* They require guessing the view hints and the number of *)
(* implicits, respectively, which we do by brute force. *)
(* Builds v p *)
-let interp_view ist v p =
+let interp_view ~clear_if_id ist v p =
let is_specialize hd =
match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in
(* We cast the pile of views p into a term p_id *)
@@ -230,25 +243,31 @@ let interp_view ist v p =
match DAst.get v with
| Glob_term.GApp (hd, rargs) when is_specialize hd ->
Ssrprinters.ppdebug (lazy Pp.(str "specialize"));
- interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr
+ interp_glob ist (mkGApp p_id rargs)
+ >>= tclKeepOpenConstr >>= tclPAIR []
| _ ->
Ssrprinters.ppdebug (lazy Pp.(str "view"));
(* We find out how to build (v p) eventually using an adaptor *)
let adaptors = AdaptorDb.(get Forward) in
Proofview.tclORELSE
- (pad_to_inductive ist v >>= fun vpad ->
+ (pad_to_inductive ist v >>= fun (vpad,clr) ->
Ssrcommon.tclFIRSTa (List.map
- (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors))
+ (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)
+ >>= tclPAIR clr)
(fun _ ->
guess_max_implicits ist v >>= fun n ->
Ssrcommon.tclFIRSTi (fun n ->
- interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n)
- >>= tclKeepOpenConstr
+ interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n
+ >>= fun x -> tclADD_CLEAR_IF_ID x x)
+ >>= fun (ot,clr) ->
+ if clear_if_id
+ then tclKeepOpenConstr ot >>= tclPAIR clr
+ else tclKeepOpenConstr ot >>= tclPAIR []
(* we store in the state (v top), then (v1 (v2 top))... *)
-let pile_up_view (ist, v) =
+let pile_up_view ~clear_if_id (ist, v) =
let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
- State.vsPUSH (fun p -> interp_view ist v p)
+ State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p)
let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
@@ -292,7 +311,7 @@ let pose_proof subject_name p =
<*>
Tactics.New.reduce_after_refine
-let rec apply_all_views ending vs s0 =
+let rec apply_all_views ~clear_if_id ending vs s0 =
match vs with
| [] -> ending s0
| v :: vs ->
@@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 =
| `Tac tac ->
Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
ending s0 <*> Tacinterp.eval_tactic tac <*>
- Ssrcommon.tacSIGMA >>= apply_all_views ending vs
+ Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs
| `Term v ->
Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
- pile_up_view v <*> apply_all_views ending vs s0
+ pile_up_view ~clear_if_id v <*>
+ apply_all_views ~clear_if_id ending vs s0
(* Entry points *********************************************************)
-let tclIPAT_VIEWS ~views:vs ~conclusion:tac =
+let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac =
let end_view_application s0 =
- State.vsCONSUME (fun name t ->
- finalize_view s0 t >>= pose_proof name <*>
- tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in
+ State.vsCONSUME (fun ~name t ~to_clear ->
+ let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in
+ finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in
tclINDEPENDENT begin
State.vsASSERT_EMPTY <*>
- Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*>
+ Ssrcommon.tacSIGMA >>=
+ apply_all_views ~clear_if_id end_view_application vs <*>
State.vsASSERT_EMPTY
end
let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac =
let ending_tac s0 =
- State.vsCONSUME (fun _ t -> finalize_view s0 ~simple_types t >>= tac) in
+ State.vsCONSUME (fun ~name:_ t ~to_clear:_ ->
+ finalize_view s0 ~simple_types t >>= tac) in
tclINDEPENDENT begin
State.vsASSERT_EMPTY <*>
- State.vsINIT subject <*>
- Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*>
+ State.vsINIT (subject,[]) <*>
+ Ssrcommon.tacSIGMA >>=
+ apply_all_views ~clear_if_id:false ending_tac vs <*>
State.vsASSERT_EMPTY
end
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index be51fe7f9b..b128a95da7 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -20,9 +20,11 @@ module AdaptorDb : sig
end
-(* Apply views to the top of the stack (intro pattern) *)
+(* Apply views to the top of the stack (intro pattern). If clear_if_id is
+ * true (default false) then views that happen to be a variable are considered
+ * as to be cleared (see the to_clear argument to the continuation) *)
val tclIPAT_VIEWS :
- views:ast_closure_term list ->
+ views:ast_closure_term list -> ?clear_if_id:bool ->
conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) ->
unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:03:35 +0000