aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml1
-rw-r--r--plugins/ltac/extratactics.ml416
-rw-r--r--plugins/ltac/g_auto.ml41
-rw-r--r--plugins/ltac/g_class.ml45
-rw-r--r--plugins/ltac/g_rewrite.ml414
-rw-r--r--plugins/ltac/pltac.ml1
-rw-r--r--plugins/ltac/pptactic.ml4
-rw-r--r--plugins/ltac/profile_ltac.ml1
-rw-r--r--plugins/ltac/rewrite.ml9
-rw-r--r--plugins/ltac/rewrite.mli1
-rw-r--r--plugins/ltac/taccoerce.mli1
-rw-r--r--plugins/ltac/tacentries.ml6
-rw-r--r--plugins/ltac/tacenv.mli1
-rw-r--r--plugins/ltac/tacintern.ml6
-rw-r--r--plugins/ltac/tacinterp.ml7
-rw-r--r--plugins/ltac/tacinterp.mli1
-rw-r--r--plugins/ltac/tactic_debug.ml14
-rw-r--r--plugins/ltac/tactic_debug.mli1
-rw-r--r--plugins/ltac/tauto.ml3
19 files changed, 45 insertions, 48 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 5d3f6df03d..bc9c300e23 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -9,7 +9,6 @@
open Util
open Names
open Term
-open EConstr
open CErrors
open Evar_refiner
open Tacmach
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..3e6ccaf84a 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -21,7 +21,6 @@ open Tacexpr
open Glob_ops
open CErrors
open Util
-open Evd
open Termops
open Equality
open Misctypes
@@ -52,8 +51,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
let replace_term ist dir_opt c cl =
with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
-let clause = Pltac.clause_dft_concl
-
TACTIC EXTEND replace
["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
-> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
@@ -815,6 +812,19 @@ TACTIC EXTEND destauto
| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
END
+(**********************************************************************)
+
+(**********************************************************************)
+(* A version of abstract constructing transparent terms *)
+(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *)
+(**********************************************************************)
+
+TACTIC EXTEND transparent_abstract
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+ Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+ Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+END
(* ********************************************************************* *)
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfa8331ff2..50e8255a67 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,7 +16,6 @@ open Pcoq.Constr
open Pltac
open Hints
open Tacexpr
-open Proofview.Notations
open Names
DECLARE PLUGIN "g_auto"
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 40f30c7943..23ce368eea 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,9 +8,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Misctypes
open Class_tactics
-open Pltac
open Stdarg
open Tacarg
open Names
@@ -85,7 +83,7 @@ TACTIC EXTEND not_evar
END
TACTIC EXTEND is_ground
- [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
+ [ "is_ground" constr(ty) ] -> [ is_ground ty ]
END
TACTIC EXTEND autoapply
@@ -95,7 +93,6 @@ END
(** TODO: DEPRECATE *)
(* A progress test that allows to see if the evars have changed *)
open Term
-open Proofview.Goal
open Proofview.Notations
let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c50100bf55..ac979bcf89 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,7 @@ open Glob_term
open Geninterp
open Extraargs
open Tacmach
-open Tacticals
+open Proofview.Notations
open Rewrite
open Stdarg
open Pcoq.Vernac_
@@ -123,15 +123,19 @@ TACTIC EXTEND rewrite_strat
END
let clsubstitute o c =
+ Proofview.Goal.enter { enter = begin fun gl ->
let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
- Tacticals.onAllHypsAndConcl
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
+ Tacticals.New.tclMAP
(fun cl ->
match cl with
- | Some id when is_tac id -> tclIDTAC
- | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
+ | Some id when is_tac id -> Tacticals.New.tclIDTAC
+ | _ -> cl_rewrite_clause c o AllOccurrences cl)
+ (None :: List.map (fun id -> Some id) hyps)
+ end }
TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
END
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae8..7e979d269d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Pcoq
(* Main entry for extensions *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 39ae1f41d2..b73b66e56f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -250,7 +250,7 @@ type 'a extra_genarg_printer =
let pr_alias_key key =
try
let prods = (KNmap.find key !prnotation_tab).pptac_prods in
- let rec pr = function
+ let pr = function
| TacTerm s -> primitive s
| TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
in
@@ -314,7 +314,7 @@ type 'a extra_genarg_printer =
| Extend.Uentry _ | Extend.Uentryl _ ->
str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
- let rec pr_targ prtac symb arg = match symb with
+ let pr_targ prtac symb arg = match symb with
| Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
prtac (1, Any) arg
| Extend.Uentryl (_, l) -> prtac (l, Any) arg
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index bcb28f77ce..a853576f25 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -136,7 +136,6 @@ let feedback_results results =
let format_sec x = (Printf.sprintf "%.3fs" x)
let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
-let padr n s = str s ++ ws (max 0 (n - utf8_length s))
let padr_with c n s =
let ulength = utf8_length s in
str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600c..5630a2d7b6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
open Vars
open Reduction
open Tacticals.New
-open Tacmach
open Tactics
open Pretype_errors
open Typeclasses
@@ -39,7 +38,7 @@ open Proofview.Notations
open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
(** Typeclass-based generalized rewriting. *)
@@ -2197,7 +2196,8 @@ let setoid_transitivity c =
(transitivity_red true c)
let setoid_symmetry_in id =
- Proofview.V82.tactic (fun gl ->
+ let open Tacmach.New in
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = project gl in
let ctype = pf_unsafe_type_of gl (mkVar id) in
let binders,concl = decompose_prod_assum sigma ctype in
@@ -2211,11 +2211,10 @@ let setoid_symmetry_in id =
let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in
let new_hyp' = mkApp (he, [| c2 ; c1 |]) in
let new_hyp = it_mkProd_or_LetIn new_hyp' binders in
- Proofview.V82.of_tactic
(tclTHENLAST
(Tactics.assert_after_replacing id new_hyp)
(tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
- gl)
+ end }
let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 7a20838a27..6683d753bc 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -14,7 +14,6 @@ open Constrexpr
open Tacexpr
open Misctypes
open Evd
-open Proof_type
open Tacinterp
(** TODO: document and clean me! *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 9c4ac52657..4a44f86d92 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -8,7 +8,6 @@
open Util
open Names
-open Term
open EConstr
open Misctypes
open Pattern
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cd8c9e471e..32750383b8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -15,7 +15,6 @@ open Genarg
open Extend
open Pcoq
open Egramml
-open Egramcoq
open Vernacexpr
open Libnames
open Nameops
@@ -88,9 +87,6 @@ let rec parse_user_entry s sep =
else
Uentry s
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
let interp_entry_name interp symb =
let rec eval = function
| Ulist1 e -> Ulist1 (eval e)
@@ -320,7 +316,7 @@ let add_tactic_notation local n prods e =
let ids = List.map_filter cons_production_parameter prods in
let prods = List.map interp_prod_item prods in
let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
- add_glob_tactic_notation local n prods false ids tac
+ add_glob_tactic_notation local ~level:n prods false ids tac
(**********************************************************************)
(* ML Tactic entries *)
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223aa..d1e2a7bbe6 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Genarg
open Names
open Tacexpr
open Geninterp
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3f83f104e9..75227def0f 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,12 +118,6 @@ let intern_constr_reference strict ist = function
GRef (loc,locate_global_with_alias lqid,None),
if strict then None else Some (CRef (r,None))
-let intern_move_location ist = function
- | MoveAfter id -> MoveAfter (intern_hyp ist id)
- | MoveBefore id -> MoveBefore (intern_hyp ist id)
- | MoveFirst -> MoveFirst
- | MoveLast -> MoveLast
-
(* Internalize an isolated reference in position of tactic *)
let intern_isolated_global_tactic_reference r =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 50f43931e9..b8c021f188 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -25,7 +25,6 @@ open Refiner
open Tacmach.New
open Tactic_debug
open Constrexpr
-open Term
open Termops
open Tacexpr
open Genarg
@@ -436,12 +435,6 @@ let interp_hyp_list_as_list ist env sigma (loc,id as x) =
let interp_hyp_list ist env sigma l =
List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l)
-let interp_move_location ist env sigma = function
- | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id)
- | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id)
- | MoveFirst -> MoveFirst
- | MoveLast -> MoveLast
-
let interp_reference ist env sigma = function
| ArgArg (_,r) -> r
| ArgVar (loc, id) ->
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 1e5f6bd42b..494f36a95a 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -8,7 +8,6 @@
open Names
open Tactic_debug
-open Term
open EConstr
open Tacexpr
open Genarg
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index dffeade298..dac15ff79e 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
+let batch = ref false
+
+open Goptions
+
+let _ =
+ declare_bool_option
+ { optsync = false;
+ optdepr = false;
+ optname = "Ltac batch debug";
+ optkey = ["Ltac";"Batch";"Debug"];
+ optread = (fun () -> !batch);
+ optwrite = (fun x -> batch := x) }
+
let rec drop_spaces inst i =
if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
else i
@@ -150,6 +163,7 @@ let rec prompt level =
begin
let open Proofview.NonLogical in
Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+ if Pervasives.(!batch) then return (DebugOn (level+1)) else
let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
Proofview.NonLogical.catch Proofview.NonLogical.read_line
begin function (e, info) -> match e with
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 7745d9b7b6..0b4d35a22a 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -10,7 +10,6 @@ open Environ
open Pattern
open Names
open Tacexpr
-open Term
open EConstr
open Evd
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index dc7ee6a234..4de2081cf8 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -10,7 +10,6 @@ open Term
open EConstr
open Hipattern
open Names
-open Pp
open Geninterp
open Misctypes
open Tacexpr
@@ -242,7 +241,7 @@ let tauto_uniform_unit_flags = {
}
(* This is the compatibility mode (not used) *)
-let tauto_legacy_flags = {
+let _tauto_legacy_flags = {
binary_mode = true;
binary_mode_bugged_detection = true;
strict_in_contravariant_hyp = true;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 19:55:36 +0000