aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.mlp2
-rw-r--r--interp/constrarg.ml11
-rw-r--r--interp/constrarg.mli35
-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
-rw-r--r--plugins/firstorder/g_ground.ml41
-rw-r--r--plugins/micromega/g_micromega.ml41
-rw-r--r--plugins/quote/g_quote.ml41
-rw-r--r--plugins/setoid_ring/g_newring.ml41
-rw-r--r--plugins/ssrmatching/ssrmatching.ml41
22 files changed, 90 insertions, 43 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index a1b3f4f25..175853d50 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -61,7 +61,7 @@ let rec mlexpr_of_symbol = function
<:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
| Uentryl (e, l) ->
assert (e = "tactic");
- let arg = get_argt <:expr< Constrarg.wit_tactic >> in
+ let arg = get_argt <:expr< Tacarg.wit_tactic >> in
<:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
let make_prod_item = function
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ca828102b..aaf33a956 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Loc
-open Tacexpr
open Misctypes
open Genarg
open Geninterp
@@ -27,14 +26,9 @@ let loc_of_or_by_notation f = function
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
-let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
+let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type =
make0 "intropattern"
-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_ident =
make0 "ident"
@@ -61,9 +55,6 @@ let wit_red_expr = make0 "redexpr"
let wit_clause_dft_concl =
make0 "clause_dft_concl"
-let wit_destruction_arg =
- make0 "destruction_arg"
-
(** Aliases *)
let wit_reference = wit_ref
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 6ccd944d4..32f2dc6f3 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -17,7 +17,6 @@ open Globnames
open Genredexpr
open Pattern
open Constrexpr
-open Tacexpr
open Misctypes
open Genarg
@@ -28,7 +27,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
val wit_int_or_var : (int or_var, int or_var, int) genarg_type
-val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_intro_pattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type
val wit_ident : Id.t uniform_genarg_type
@@ -38,50 +37,38 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
+val wit_constr : (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type
-val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
+val wit_uconstr : (constr_expr , Tacexpr.glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
val wit_open_constr :
- (constr_expr, glob_constr_and_expr, constr) genarg_type
+ (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type
val wit_constr_with_bindings :
(constr_expr with_bindings,
- glob_constr_and_expr with_bindings,
- constr with_bindings delayed_open) genarg_type
+ Tacexpr.glob_constr_and_expr with_bindings,
+ constr with_bindings Pretyping.delayed_open) genarg_type
val wit_bindings :
(constr_expr bindings,
- glob_constr_and_expr bindings,
- constr bindings delayed_open) genarg_type
+ Tacexpr.glob_constr_and_expr bindings,
+ constr bindings Pretyping.delayed_open) genarg_type
val wit_red_expr :
((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
- (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+ (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen,
(constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-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_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
-val wit_destruction_arg :
- (constr_expr with_bindings destruction_arg,
- glob_constr_and_expr with_bindings destruction_arg,
- delayed_open_constr_with_bindings destruction_arg) genarg_type
-
(** Aliases for compatibility *)
val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type
val wit_redexpr :
((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
- (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+ (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen,
(constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index c32f757d9..1176772cd 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 d16ed84a2..de701bb23 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 3cdb3a6c7..b662057ba 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 f17cbc9a3..cce068910 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 df0b3e855..fd531ca69 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 b9b63be3a..029dfd393 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 148867aac..94bf32d1d 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 a4222ae2c..dc2676bf4 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 000000000..42552c484
--- /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 000000000..bfa423db2
--- /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 fcdb1875d..2e2b55be7 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 b1de30893..b0b4dc357 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 9e502682b..a65e58ddb 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 cce4382c2..e0fdc4e5a 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
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 95095b09c..487162687 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -16,6 +16,7 @@ open Tacticals
open Tacinterp
open Libnames
open Constrarg
+open Tacarg
open Stdarg
open Pcoq.Prim
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 027f690fc..aadcf060e 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -17,6 +17,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Constrarg
+open Tacarg
DECLARE PLUGIN "micromega_plugin"
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index fd87d5b7d..ebd19428f 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -14,6 +14,7 @@ open Tacexpr
open Geninterp
open Quote
open Constrarg
+open Tacarg
DECLARE PLUGIN "quote_plugin"
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 1a0020031..13e225404 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -16,6 +16,7 @@ open Newring_ast
open Newring
open Stdarg
open Constrarg
+open Tacarg
open Pcoq.Constr
open Pltac
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 150be9d72..099918c35 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -20,6 +20,7 @@ open Pp
open Pcoq
open Genarg
open Constrarg
+open Tacarg
open Term
open Vars
open Topconstr
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 03:15:24 +0000