aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/extraargs.ml41
-rw-r--r--ltac/extratactics.ml41
-rw-r--r--ltac/g_class.ml41
-rw-r--r--ltac/g_ltac.ml45
-rw-r--r--ltac/g_obligations.ml41
-rw-r--r--ltac/ltac.mllib1
-rw-r--r--ltac/pltac.ml1
-rw-r--r--ltac/pptactic.ml3
-rw-r--r--ltac/tacarg.ml26
-rw-r--r--ltac/tacarg.mli27
-rw-r--r--ltac/tacentries.ml10
-rw-r--r--ltac/tacintern.ml1
-rw-r--r--ltac/tacinterp.ml1
-rw-r--r--ltac/tacsubst.ml1
14 files changed, 72 insertions, 8 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index c32f757d9c..1176772cdc 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -12,6 +12,7 @@ open Pp
open Genarg
open Stdarg
open Constrarg
+open Tacarg
open Pcoq.Prim
open Pcoq.Constr
open Names
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d16ed84a24..de701bb239 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -12,6 +12,7 @@ open Pp
open Genarg
open Stdarg
open Constrarg
+open Tacarg
open Extraargs
open Pcoq.Prim
open Pltac
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 3cdb3a6c7d..b662057ba3 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -13,6 +13,7 @@ open Class_tactics
open Pltac
open Stdarg
open Constrarg
+open Tacarg
DECLARE PLUGIN "g_class"
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index f17cbc9a3b..cce0689107 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -34,7 +34,7 @@ let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
-let in_tac tac = in_gen (rawwit Constrarg.wit_ltac) tac
+let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
let reference_to_id = function
| Libnames.Ident (loc, id) -> (loc, id)
@@ -348,12 +348,13 @@ GEXTEND Gram
;
operconstr: LEVEL "0"
[ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
- let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
+ let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
;
END
open Constrarg
+open Tacarg
open Vernacexpr
open Vernac_classifier
open Goptions
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index df0b3e855e..fd531ca691 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -18,6 +18,7 @@ open Constrexpr
open Constrexpr_ops
open Stdarg
open Constrarg
+open Tacarg
open Extraargs
let (set_default_tactic, get_default_tactic, print_default_tactic) =
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index b9b63be3aa..029dfd393f 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -1,3 +1,4 @@
+Tacarg
Pptactic
Pltac
Taccoerce
diff --git a/ltac/pltac.ml b/ltac/pltac.ml
index 148867aacb..94bf32d1d5 100644
--- a/ltac/pltac.ml
+++ b/ltac/pltac.ml
@@ -50,6 +50,7 @@ let tactic_eoi = eoi_entry tactic
let () =
let open Stdarg in
let open Constrarg in
+ let open Tacarg in
register_grammar wit_int_or_var (int_or_var);
register_grammar wit_intro_pattern (simple_intropattern);
register_grammar wit_quant_hyp (quantified_hypothesis);
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index a4222ae2ca..dc2676bf4b 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -16,6 +16,7 @@ open Tacexpr
open Genarg
open Geninterp
open Constrarg
+open Tacarg
open Libnames
open Ppextend
open Misctypes
@@ -1305,7 +1306,7 @@ let () =
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
(pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
(fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
- Genprint.register_print0 Constrarg.wit_destruction_arg
+ Genprint.register_print0 Tacarg.wit_destruction_arg
(pr_destruction_arg pr_constr_expr pr_lconstr_expr)
(pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
(fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it));
diff --git a/ltac/tacarg.ml b/ltac/tacarg.ml
new file mode 100644
index 0000000000..42552c4846
--- /dev/null
+++ b/ltac/tacarg.ml
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Generic arguments based on Ltac. *)
+
+open Genarg
+open Geninterp
+open Tacexpr
+
+let make0 ?dyn name =
+ let wit = Genarg.make0 name in
+ let () = Geninterp.register_val0 wit dyn in
+ wit
+
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
+ make0 "tactic"
+
+let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
+
+let wit_destruction_arg =
+ make0 "destruction_arg"
diff --git a/ltac/tacarg.mli b/ltac/tacarg.mli
new file mode 100644
index 0000000000..bfa423db20
--- /dev/null
+++ b/ltac/tacarg.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Genarg
+open Tacexpr
+open Constrexpr
+open Misctypes
+
+(** Generic arguments based on Ltac. *)
+
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
+
+(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
+ toplevel interpretation. The one of [wit_ltac] forces the tactic and
+ discards the result. *)
+val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
+
+val wit_destruction_arg :
+ (constr_expr with_bindings Tacexpr.destruction_arg,
+ glob_constr_and_expr with_bindings Tacexpr.destruction_arg,
+ delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type
+
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index fcdb1875d0..2e2b55be74 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -56,9 +56,9 @@ let get_tacentry n m =
&& not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
&& not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
in
- if check_lvl n then EntryName (rawwit Constrarg.wit_tactic, Aself)
- else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext)
- else EntryName (rawwit Constrarg.wit_tactic, atactic n)
+ if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
+ else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+ else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
| None -> error "Missing separator."
@@ -163,7 +163,7 @@ let add_tactic_entry (kn, ml, tg) state =
let mkact loc l =
let map arg =
(** HACK to handle especially the tactic(...) entry *)
- let wit = Genarg.rawwit Constrarg.wit_tactic in
+ let wit = Genarg.rawwit Tacarg.wit_tactic in
if Genarg.has_type arg wit && not ml then
Tacexp (Genarg.out_gen wit arg)
else
@@ -218,7 +218,7 @@ let interp_prod_item = function
| Some n ->
(** FIXME: do better someday *)
assert (String.equal s "tactic");
- begin match Constrarg.wit_tactic with
+ begin match Tacarg.wit_tactic with
| ExtraArg tag -> ArgT.Any tag
| _ -> assert false
end
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index b1de30893d..b0b4dc3579 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -24,6 +24,7 @@ open Termops
open Tacexpr
open Genarg
open Constrarg
+open Tacarg
open Misctypes
open Locus
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 9e502682b8..a65e58ddb0 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -32,6 +32,7 @@ open Genarg
open Geninterp
open Stdarg
open Constrarg
+open Tacarg
open Printer
open Pretyping
open Misctypes
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index cce4382c2c..e0fdc4e5a1 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -11,6 +11,7 @@ open Tacexpr
open Mod_subst
open Genarg
open Constrarg
+open Tacarg
open Misctypes
open Globnames
open Term
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 04:00:14 +0000