aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib1
-rw-r--r--grammar/grammar.mllib1
-rw-r--r--grammar/tacextend.ml41
-rw-r--r--interp/constrarg.ml8
-rw-r--r--interp/constrarg.mli2
-rw-r--r--parsing/extrawit.ml44
-rw-r--r--parsing/extrawit.mli27
-rw-r--r--parsing/parsing.mllib1
-rw-r--r--parsing/pcoq.ml436
-rw-r--r--printing/ppextra.ml20
-rw-r--r--printing/pptactic.ml4
-rw-r--r--tactics/tacintern.ml5
-rw-r--r--tactics/tacinterp.ml26
-rw-r--r--tactics/tacsubst.ml4
-rw-r--r--toplevel/toplevel.mllib1
15 files changed, 52 insertions, 129 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 3a8a2cc3d..c3d3ce709 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -155,7 +155,6 @@ Pfedit
Tactic_debug
Decl_mode
Ppconstr
-Extrawit
Pcoq
Printer
Pptactic
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index f361bee49..bde5c15f3 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -31,7 +31,6 @@ Stdarg
Constrarg
Tok
Lexer
-Extrawit
Pcoq
Q_util
Q_coqast
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 1b29da681..d494a92d8 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -15,7 +15,6 @@ open Q_util
open Q_coqast
open Argextend
open Pcoq
-open Extrawit
open Egramml
open Compat
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 87da56e4f..5c2b3392c 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -14,6 +14,7 @@ open Libnames
open Globnames
open Glob_term
open Genredexpr
+open Tacexpr
open Pattern
open Constrexpr
open Term
@@ -35,6 +36,9 @@ let wit_int_or_var = unsafe_of_type IntOrVarArgType
let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type =
Genarg.make0 None "intropattern"
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
+ Genarg.make0 None "tactic"
+
let wit_ident_gen b = unsafe_of_type (IdentArgType b)
let wit_ident = wit_ident_gen true
@@ -69,4 +73,6 @@ let wit_red_expr = unsafe_of_type RedExprArgType
(** Register location *)
-let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"
+let () =
+ register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
+ register_name0 wit_tactic "Constrarg.wit_tactic"
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 548bd6690..1233e165f 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -77,3 +77,5 @@ 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,
(constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
+
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
deleted file mode 100644
index c20f43bd5..000000000
--- a/parsing/extrawit.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Pp
-open Genarg
-
-(* This file defines extra argument types *)
-
-(* Tactics as arguments *)
-
-let tactic_main_level = 5
-
-let wit_tactic0 = create_arg None "tactic0"
-let wit_tactic1 = create_arg None "tactic1"
-let wit_tactic2 = create_arg None "tactic2"
-let wit_tactic3 = create_arg None "tactic3"
-let wit_tactic4 = create_arg None "tactic4"
-let wit_tactic5 = create_arg None "tactic5"
-
-let wit_tactic = function
- | 0 -> wit_tactic0
- | 1 -> wit_tactic1
- | 2 -> wit_tactic2
- | 3 -> wit_tactic3
- | 4 -> wit_tactic4
- | 5 -> wit_tactic5
- | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
-
-let tactic_genarg_level s =
- if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then
- let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
- else None
- else None
-
-let () =
- for i = 0 to 5 do
- let name = Printf.sprintf "Extrawit.wit_tactic%i" i in
- Genarg.register_name0 (wit_tactic i) name
- done
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
deleted file mode 100644
index 1bd5cdb89..000000000
--- a/parsing/extrawit.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Genarg
-open Tacexpr
-
-(** This file defines extra argument types *)
-
-(** Tactics as arguments *)
-
-val tactic_main_level : int
-
-val wit_tactic : int -> (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-
-val wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-val wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-
-val tactic_genarg_level : string -> int option
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 2f0851164..500d7dde9 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,7 +1,6 @@
Tok
Compat
Lexer
-Extrawit
Pcoq
Egramml
Egramcoq
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2769612d5..211bf2632 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -16,7 +16,6 @@ open Genarg
open Stdarg
open Constrarg
open Tacexpr
-open Extrawit
(** The parser of Coq *)
@@ -398,7 +397,7 @@ module Tactic =
let tactic_expr = Gram.entry_create "tactic:tactic_expr"
let binder_tactic = Gram.entry_create "tactic:binder_tactic"
- let tactic = make_gen_entry utactic (rawwit (wit_tactic tactic_main_level)) "tactic"
+ let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
@@ -756,6 +755,15 @@ let coincide s pat off =
done;
!break
+let tactic_level s =
+ if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then
+ let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
+ else None
+ else None
+
+let type_of_entry u s =
+ type_of_typed_entry (get_entry u s)
+
let rec interp_entry_name static up_level s sep =
let l = String.length s in
if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
@@ -784,20 +792,26 @@ let rec interp_entry_name static up_level s sep =
| Some m -> Int.equal m n && not (Int.equal m 5)
in
let t, se =
- match Extrawit.tactic_genarg_level s with
- | Some n when check_lvl n -> None, Aself
- | Some n when check_lvl (n + 1) -> None, Anext
- | Some n -> None, Atactic n
- | None ->
- try Some (get_entry uprim s), Aentry ("prim",s) with Not_found ->
- try Some (get_entry uconstr s), Aentry ("constr",s) with Not_found ->
- try Some (get_entry utactic s), Aentry ("tactic",s) with Not_found ->
+ match tactic_level s with
+ | Some n ->
+ (** Quite ad-hoc *)
+ let t = unquote (rawwit wit_tactic) in
+ let se =
+ if check_lvl n then Aself
+ else if check_lvl (n + 1) then Anext
+ else Atactic n
+ in
+ (Some t, se)
+ | None ->
+ try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found ->
+ try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found ->
+ try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found ->
if static then
error ("Unknown entry "^s^".")
else
None, Aentry ("",s) in
let t =
match t with
- | Some t -> type_of_typed_entry t
+ | Some t -> t
| None -> ExtraArgType s in
t, se
diff --git a/printing/ppextra.ml b/printing/ppextra.ml
deleted file mode 100644
index 8acdd2e1b..000000000
--- a/printing/ppextra.ml
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Genarg
-open Ppextend
-open Pptactic
-open Extrawit
-
-let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
-
-let _ = for i=0 to 5 do
- let wit = wit_tactic i in
- declare_extra_genarg_pprule wit
- (pr_tac_polymorphic i) (pr_tac_polymorphic i) (pr_tac_polymorphic i)
-done
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 3b3de2a3c..0fd3b454c 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1011,6 +1011,10 @@ let register_uniform_printer wit pr =
let () = Genprint.register_print0 Constrarg.wit_intro_pattern
pr_intro_pattern pr_intro_pattern pr_intro_pattern
+let () =
+ let printer _ _ prtac = prtac (0, E) in
+ declare_extra_genarg_pprule wit_tactic printer printer printer
+
let _ = Hook.set Tactic_debug.tactic_printer
(fun x -> pr_glob_tactic (Global.env()) x)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6d50c02e2..1a63ca2da 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -27,7 +27,6 @@ open Tacexpr
open Genarg
open Constrarg
open Mod_subst
-open Extrawit
open Misctypes
open Locus
@@ -950,9 +949,7 @@ let () =
let () =
let intern ist tac = (ist, intern_tactic_or_tacarg ist tac) in
- for i = 0 to 5 do
- Genintern.register_intern0 (wit_tactic i) intern
- done
+ Genintern.register_intern0 wit_tactic intern
(***************************************************************************)
(* Backwarding recursive needs of tactic glob/interp/eval functions *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 67fa0ed7b..d5c48f9e6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -37,7 +37,6 @@ open Stdarg
open Constrarg
open Printer
open Pretyping
-open Extrawit
open Evd
open Misctypes
open Miscops
@@ -1910,13 +1909,6 @@ and interp_atomic ist gl tac =
let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
evdref := sigma;
Value.of_constr c_interp
- | ExtraArgType s when not (Option.is_empty (tactic_genarg_level s)) ->
- (* Special treatment of tactic arguments *)
- let (sigma,v) = val_interp ist gl
- (out_gen (glbwit (wit_tactic (Option.get (tactic_genarg_level s)))) x)
- in
- evdref := sigma;
- v
| List0ArgType ConstrArgType ->
let wit = glbwit (wit_list0 wit_constr) in
let (sigma,l_interp) =
@@ -1966,9 +1958,17 @@ and interp_atomic ist gl tac =
| List0ArgType _ -> app_list0 f x
| List1ArgType _ -> app_list1 f x
| ExtraArgType _ ->
- let (sigma, v) = Geninterp.generic_interp ist { gl with sigma = !evdref } x in
- evdref := sigma;
- v
+ (** Special treatment of tactics *)
+ let gl = { gl with sigma = !evdref } in
+ if has_type x (glbwit wit_tactic) then
+ let tac = out_gen (glbwit wit_tactic) x in
+ let (sigma, v) = val_interp ist gl tac in
+ let () = evdref := sigma in
+ v
+ else
+ let (sigma, v) = Geninterp.generic_interp ist gl x in
+ let () = evdref := sigma in
+ v
| QuantHypArgType | RedExprArgType
| OpenConstrArgType _ | ConstrWithBindingsArgType
| BindingsArgType
@@ -2064,9 +2064,7 @@ let () =
let f = VFun (extract_trace ist, ist.lfun, [], tac) in
(gl.sigma, TacArg (dloc, valueIn (of_tacvalue f)))
in
- for i = 0 to 5 do
- Geninterp.register_interp0 (wit_tactic i) interp
- done
+ Geninterp.register_interp0 wit_tactic interp
(***************************************************************************)
(* Other entry points *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 006885616..11b747e72 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -329,8 +329,6 @@ and subst_genarg subst (x:glob_generic_argument) =
let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v)
let () =
- for i = 0 to 5 do
- Genintern.register_subst0 (Extrawit.wit_tactic i) subst_tactic
- done
+ Genintern.register_subst0 wit_tactic subst_tactic
let _ = Hook.set Auto.extern_subst_tactic subst_tactic
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index a3da105ae..b27c7588d 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -12,7 +12,6 @@ Obligations
Command
Classes
Record
-Ppextra
Ppvernac
Backtrack
Vernacinterp
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:10:37 +0000