aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml4
-rw-r--r--plugins/ltac/extraargs.ml4102
-rw-r--r--plugins/ltac/extraargs.mli5
-rw-r--r--plugins/ltac/extratactics.ml421
-rw-r--r--plugins/ltac/g_ltac.ml414
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ltac/plugin_base.dune13
-rw-r--r--plugins/ltac/pptactic.ml7
-rw-r--r--plugins/ltac/rewrite.ml5
-rw-r--r--plugins/ltac/tacentries.ml11
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tacenv.mli2
-rw-r--r--plugins/ltac/tacexpr.ml13
-rw-r--r--plugins/ltac/tacexpr.mli11
-rw-r--r--plugins/ltac/tacintern.ml1
-rw-r--r--plugins/ltac/tacinterp.ml29
-rw-r--r--plugins/ltac/tacsubst.ml1
-rw-r--r--plugins/ltac/tactic_debug.ml2
18 files changed, 100 insertions, 145 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 84f13d2131..b0277e9cc2 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -94,12 +94,12 @@ let let_evar name typ =
in
let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
+ (Tactics.pose_tac (Name.Name id) evar)
end
let hget_evar n =
let open EConstr in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let evl = evar_list sigma concl in
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dbbdbfa396..f4555509cc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -52,8 +52,11 @@ let () =
(* Rewriting orientation *)
-let _ = Metasyntax.add_token_obj "<-"
-let _ = Metasyntax.add_token_obj "->"
+let _ =
+ Mltop.declare_cache_obj
+ (fun () -> Metasyntax.add_token_obj "<-";
+ Metasyntax.add_token_obj "->")
+ "ltac_plugin"
let pr_orient _prc _prlc _prt = function
| true -> Pp.mt ()
@@ -196,9 +199,9 @@ let pr_gen_place pr_id = function
ConclLocation () -> Pp.mt ()
| HypLocation (id,InHyp) -> str "in " ++ pr_id id
| HypLocation (id,InHypTypeOnly) ->
- str "in (Type of " ++ pr_id id ++ str ")"
+ str "in (type of " ++ pr_id id ++ str ")"
| HypLocation (id,InHypValueOnly) ->
- str "in (Value of " ++ pr_id id ++ str ")"
+ str "in (value of " ++ pr_id id ++ str ")"
let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id)
let pr_place _ _ _ = pr_gen_place Id.print
@@ -217,6 +220,14 @@ let interp_place ist gl p =
let subst_place subst pl = pl
+let warn_deprecated_instantiate_syntax =
+ CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated"
+ (fun (v,v',id) ->
+ let s = Id.to_string id in
+ Pp.strbrk
+ ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".")
+ )
+
ARGUMENT EXTEND hloc
PRINTED BY pr_place
INTERPRETED BY interp_place
@@ -231,8 +242,14 @@ ARGUMENT EXTEND hloc
| [ "in" ident(id) ] ->
[ HypLocation ((CAst.make id),InHyp) ]
| [ "in" "(" "Type" "of" ident(id) ")" ] ->
- [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+ [ warn_deprecated_instantiate_syntax ("Type","type",id);
+ HypLocation ((CAst.make id),InHypTypeOnly) ]
| [ "in" "(" "Value" "of" ident(id) ")" ] ->
+ [ warn_deprecated_instantiate_syntax ("Value","value",id);
+ HypLocation ((CAst.make id),InHypValueOnly) ]
+| [ "in" "(" "type" "of" ident(id) ")" ] ->
+ [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+| [ "in" "(" "value" "of" ident(id) ")" ] ->
[ HypLocation ((CAst.make id),InHypValueOnly) ]
END
@@ -294,78 +311,3 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
| [ local_test_lpar_id_colon(x) ] -> [ () ]
END
-
-(* spiwack: the print functions are incomplete, but I don't know what they are
- used for *)
-let pr_r_int31_field i31f =
- str "int31 " ++
- match i31f with
- | Retroknowledge.Int31Bits -> str "bits"
- | Retroknowledge.Int31Type -> str "type"
- | Retroknowledge.Int31Twice -> str "twice"
- | Retroknowledge.Int31TwicePlusOne -> str "twice plus one"
- | Retroknowledge.Int31Phi -> str "phi"
- | Retroknowledge.Int31PhiInv -> str "phi inv"
- | Retroknowledge.Int31Plus -> str "plus"
- | Retroknowledge.Int31Times -> str "times"
- | Retroknowledge.Int31Constructor -> assert false
- | Retroknowledge.Int31PlusC -> str "plusc"
- | Retroknowledge.Int31PlusCarryC -> str "pluscarryc"
- | Retroknowledge.Int31Minus -> str "minus"
- | Retroknowledge.Int31MinusC -> str "minusc"
- | Retroknowledge.Int31MinusCarryC -> str "minuscarryc"
- | Retroknowledge.Int31TimesC -> str "timesc"
- | Retroknowledge.Int31Div21 -> str "div21"
- | Retroknowledge.Int31Div -> str "div"
- | Retroknowledge.Int31Diveucl -> str "diveucl"
- | Retroknowledge.Int31AddMulDiv -> str "addmuldiv"
- | Retroknowledge.Int31Compare -> str "compare"
- | Retroknowledge.Int31Head0 -> str "head0"
- | Retroknowledge.Int31Tail0 -> str "tail0"
- | Retroknowledge.Int31Lor -> str "lor"
- | Retroknowledge.Int31Land -> str "land"
- | Retroknowledge.Int31Lxor -> str "lxor"
-
-let pr_retroknowledge_field f =
- match f with
- (* | Retroknowledge.KEq -> str "equality"
- | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf
- | Retroknowledge.KN nf -> pr_r_n_field () () () nf *)
- | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
- spc () ++ str "in " ++ qs group
-
-VERNAC ARGUMENT EXTEND retroknowledge_int31
-PRINTED BY pr_r_int31_field
-| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
-| [ "int31" "type" ] -> [ Retroknowledge.Int31Type ]
-| [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ]
-| [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ]
-| [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ]
-| [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ]
-| [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ]
-| [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ]
-| [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ]
-| [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ]
-| [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ]
-| [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ]
-| [ "int31" "times" ] -> [ Retroknowledge.Int31Times ]
-| [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ]
-| [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ]
-| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ]
-| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ]
-| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ]
-| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
-| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ]
-| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ]
-| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ]
-| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ]
-| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ]
-END
-
-VERNAC ARGUMENT EXTEND retroknowledge_field
-PRINTED BY pr_retroknowledge_field
-(*| [ "equality" ] -> [ Retroknowledge.KEq ]
-| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ]
-| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*)
-| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ]
-END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e477b12cd3..fa70235975 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t
val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
-(** Spiwack: Primitive for retroknowledge registration *)
-
-val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
-val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
-
val wit_in_clause :
(lident Locus.clause_expr,
lident Locus.clause_expr,
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index dc027c4041..ba3fa6fa0d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -26,6 +26,7 @@ open Termops
open Equality
open Namegen
open Tactypes
+open Tactics
open Proofview.Notations
open Vernacinterp
@@ -545,22 +546,6 @@ END
(**********************************************************************)
-(*spiwack : Vernac commands for retroknowledge *)
-
-VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
- | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
- [ let env = Global.env () in
- let evd = Evd.from_env env in
- let tc,_ctx = Constrintern.interp_constr env evd c in
- let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
- let tc = EConstr.to_constr evd tc in
- let tb = EConstr.to_constr evd tb in
- Global.register f tc tb ]
-END
-
-
-
-(**********************************************************************)
(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
defined by Conor McBride *)
TACTIC EXTEND generalize_eqs
@@ -796,9 +781,9 @@ END
(**********************************************************************)
TACTIC EXTEND transparent_abstract
-| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl ->
Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ]
-| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl ->
Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ]
END
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index c13bd69daf..929390b1c4 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -314,22 +314,23 @@ GEXTEND Gram
range_selector_or_nth:
[ [ n = natural ; "-" ; m = natural;
l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
- SelectList ((n, m) :: Option.default [] l)
+ Goal_select.SelectList ((n, m) :: Option.default [] l)
| n = natural;
l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
+ let open Goal_select in
Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ]
;
selector_body:
[ [ l = range_selector_or_nth -> l
- | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ]
+ | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ]
;
selector:
[ [ IDENT "only"; sel = selector_body; ":" -> sel ] ]
;
toplevel_selector:
[ [ sel = selector_body; ":" -> sel
- | "!"; ":" -> SelectAlreadyFocused
- | IDENT "all"; ":" -> SelectAll ] ]
+ | "!"; ":" -> Goal_select.SelectAlreadyFocused
+ | IDENT "all"; ":" -> Goal_select.SelectAll ] ]
;
tactic_mode:
[ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g
@@ -346,7 +347,7 @@ GEXTEND Gram
hint:
[ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
tac = Pltac.tactic ->
- Vernacexpr.HintsExtern (n,c, in_tac tac) ] ]
+ Hints.HintsExtern (n,c, in_tac tac) ] ]
;
operconstr: LEVEL "0"
[ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
@@ -373,6 +374,7 @@ let _ = declare_int_option {
}
let vernac_solve n info tcom b =
+ let open Goal_select in
let status = Proof_global.with_current_proof (fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
@@ -432,7 +434,7 @@ VERNAC tactic_mode EXTEND VernacSolve
VtLater
] -> [
let t = rm_abstract t in
- vernac_solve SelectAll n t def
+ vernac_solve Goal_select.SelectAll n t def
]
END
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 2e1ce814aa..571595be70 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -21,6 +21,8 @@ open Constrexpr
open Libnames
open Tok
open Tactypes
+open Tactics
+open Inv
open Locus
open Decl_kinds
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
new file mode 100644
index 0000000000..5611f5ba16
--- /dev/null
+++ b/plugins/ltac/plugin_base.dune
@@ -0,0 +1,13 @@
+(library
+ (name ltac_plugin)
+ (public_name coq.plugins.ltac)
+ (synopsis "Coq's LTAC tactic language")
+ (modules :standard \ tauto)
+ (libraries coq.stm))
+
+(library
+ (name tauto_plugin)
+ (public_name coq.plugins.tauto)
+ (synopsis "Coq's tauto tactic")
+ (modules tauto)
+ (libraries coq.plugins.ltac))
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 4357689ee2..b219ee25ca 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -28,6 +28,7 @@ open Printer
open Tacexpr
open Tacarg
+open Tactics
module Tag =
struct
@@ -271,6 +272,8 @@ let string_of_genarg_arg (ArgumentType arg) =
in
pr_sequence pr prods
with Not_found ->
+ (* FIXME: This key, moreover printed with a low-level printer,
+ has no meaning user-side *)
KerName.print key
let pr_alias_gen pr_gen lev key l =
@@ -507,7 +510,7 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_destruction_arg prc prlc (clear_flag,h) =
pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
- let pr_inversion_kind = function
+ let pr_inversion_kind = let open Inv in function
| SimpleInversion -> primitive "simple inversion"
| FullInversion -> primitive "inversion"
| FullInversionClear -> primitive "inversion_clear"
@@ -516,7 +519,7 @@ let string_of_genarg_arg (ArgumentType arg) =
if Int.equal i j then int i
else int i ++ str "-" ++ int j
-let pr_goal_selector toplevel = function
+let pr_goal_selector toplevel = let open Goal_select in function
| SelectAlreadyFocused -> str "!:"
| SelectNth i -> int i ++ str ":"
| SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9f8cd2fc4e..5b8bd6d01a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -520,11 +520,6 @@ let rewrite_db = "rewrite"
let conv_transparent_state = (Id.Pred.empty, Cpred.full)
-let _ =
- Hints.add_hints_init
- (fun () ->
- Hints.create_hint_db false rewrite_db conv_transparent_state true)
-
let rewrite_transparent_state () =
Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4b834d66d3..636cb8ebf8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -594,15 +594,6 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol
let clause_of_ty_ml = function
| TyML (t,_) -> clause_of_sign t
-let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
- | TUentry a -> ExtraArg a
- | TUentryl (a,l) -> ExtraArg a
- | TUopt(o) -> OptArg (prj o)
- | TUlist1 l -> ListArg (prj l)
- | TUlist1sep (l,_) -> ListArg (prj l)
- | TUlist0 l -> ListArg (prj l)
- | TUlist0sep (l,_) -> ListArg (prj l)
-
let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
fun sign tac ->
match sign with
@@ -617,7 +608,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
begin fun tac vals ist -> match vals with
| [] -> assert false
| v :: vals ->
- let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+ let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in
f (tac v') vals ist
end tac
| TyAnonArg (a, sig') -> eval_sign sig' tac
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 0bb9ccb1d8..1f2c722b34 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -144,7 +144,7 @@ let add ~deprecation kn b t =
mactab := KNmap.add kn entry !mactab
let replace kn path t =
- let (path, _, _) = KerName.repr path in
+ let path = KerName.modpath path in
let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
mactab := KNmap.modify kn entry !mactab
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 7143f51853..d5d36c97fa 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -41,7 +41,7 @@ val register_alias : alias -> alias_tactic -> unit
(** Register a tactic alias. *)
val interp_alias : alias -> alias_tactic
-(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+(** Recover the body of an alias. Raises an anomaly if it does not exist. *)
val check_alias : alias -> bool
(** Returns [true] if an alias is defined, false otherwise. *)
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 59b748e25e..11d13d3a2f 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -37,16 +37,24 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use
type goal_selector = Goal_select.t =
| SelectAlreadyFocused
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectNth of int
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectList of (int * int) list
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectId of Id.t
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectAll
-[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
+[@@ocaml.deprecated "Use [Goal_select.t]"]
type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
| ElimOnConstr of 'a
+ [@ocaml.deprecated "Use constructors in [Tactics]"]
| ElimOnIdent of lident
+ [@ocaml.deprecated "Use constructors in [Tactics]"]
| ElimOnAnonHyp of int
+ [@ocaml.deprecated "Use constructors in [Tactics]"]
[@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
type 'a destruction_arg =
@@ -55,8 +63,11 @@ type 'a destruction_arg =
type inversion_kind = Inv.inversion_kind =
| SimpleInversion
+ [@ocaml.deprecated "Use constructors in [Inv]"]
| FullInversion
+ [@ocaml.deprecated "Use constructors in [Inv]"]
| FullInversionClear
+ [@ocaml.deprecated "Use constructors in [Inv]"]
[@@ocaml.deprecated "Use Tactics.inversion_kind"]
type ('c,'d,'id) inversion_strength =
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 3a0badb28f..6b131edaac 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -37,16 +37,24 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use
type goal_selector = Goal_select.t =
| SelectAlreadyFocused
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectNth of int
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectList of (int * int) list
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectId of Id.t
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
| SelectAll
+ [@ocaml.deprecated "Use constructors in [Goal_select]"]
[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
| ElimOnConstr of 'a
+ [@ocaml.deprecated "Use constructors in [Tactics]"]
| ElimOnIdent of lident
+ [@ocaml.deprecated "Use constructors in [Tactics]"]
| ElimOnAnonHyp of int
+ [@ocaml.deprecated "Use constructors in [Tactics]"]
[@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
type 'a destruction_arg =
@@ -55,8 +63,11 @@ type 'a destruction_arg =
type inversion_kind = Inv.inversion_kind =
| SimpleInversion
+ [@ocaml.deprecated "Use constructors in [Inv]"]
| FullInversion
+ [@ocaml.deprecated "Use constructors in [Inv]"]
| FullInversionClear
+ [@ocaml.deprecated "Use constructors in [Inv]"]
[@@ocaml.deprecated "Use Tactics.inversion_kind"]
type ('c,'d,'id) inversion_strength =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 1444800624..5501cf92a5 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -29,6 +29,7 @@ open Stdarg
open Tacarg
open Namegen
open Tactypes
+open Tactics
open Locus
(** Globalization of tactic expressions :
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a0446bd6a0..9f34df4608 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -37,6 +37,7 @@ open Tacarg
open Printer
open Pretyping
open Tactypes
+open Tactics
open Locus
open Tacintern
open Taccoerce
@@ -1297,7 +1298,7 @@ and tactic_of_value ist vle =
match appl with
UnnamedAppl -> "An unnamed user-defined tactic"
| GlbAppl apps ->
- let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in
+ let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in
match nms with
[] -> assert false
| kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *)
@@ -1468,7 +1469,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
independently of goals. *)
and interp_genarg_constr_list ist x =
- Ftactic.nf_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
@@ -1600,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacMutualFix (id,n,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,n,c) =
let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1615,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacMutualCofix (id,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1664,16 +1665,18 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* We try to fully-typecheck the term *)
let flags = open_constr_use_classes_flags () in
let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
- let let_tac b na c cl eqpat =
- let id = Option.default (make IntroAnonymous) eqpat in
- let with_eq = if b then None else Some (true,id) in
- Tactics.letin_tac with_eq na c None cl
- in
let na = interp_name ist env sigma na in
+ let let_tac =
+ if b then Tactics.pose_tac na c_interp
+ else
+ let id = Option.default (make IntroAnonymous) eqpat in
+ let with_eq = Some (true, id) in
+ Tactics.letin_tac with_eq na c_interp None Locusops.nowhere
+ in
Tacticals.New.tclWITHHOLES ev
(name_atomic ~env
(TacLetTac(ev,na,c_interp,clp,b,eqpat))
- (let_tac b na c_interp clp eqpat)) sigma
+ let_tac) sigma
else
(* We try to keep the pattern structure as much as possible *)
let let_pat_tac b na c cl eqpat =
@@ -1693,7 +1696,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInductionDestruct (isrec,ev,(l,el)) ->
(* spiwack: some unknown part of destruct needs the goal to be
prenormalised. *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma,l =
@@ -1720,7 +1723,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Conversion *)
| TacReduce (r,cl) ->
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
@@ -2029,7 +2032,7 @@ let _ =
let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
(EConstr.of_constr c, sigma)
in
- Pretyping.register_constr_interp0 wit_tactic eval
+ GlobEnv.register_constr_interp0 wit_tactic eval
let vernac_debug b =
set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index dd799dc131..4626378db6 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -15,6 +15,7 @@ open Genarg
open Stdarg
open Tacarg
open Tactypes
+open Tactics
open Globnames
open Genredexpr
open Patternops
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 105b5c59ae..48d677a864 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -58,7 +58,7 @@ let db_pr_goal gl =
str" " ++ pc) ++ fnl ()
let db_pr_goal =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let pg = db_pr_goal gl in
Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 23:19:58 +0000