aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli1
-rw-r--r--parsing/g_vernac.ml46
-rw-r--r--parsing/pcoq.ml3
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--printing/ppvernac.ml23
-rw-r--r--stm/texmacspp.ml1
-rw-r--r--stm/vernac_classifier.ml7
-rw-r--r--tactics/g_ltac.ml418
-rw-r--r--tactics/tacentries.ml77
-rw-r--r--tactics/tacentries.mli2
-rw-r--r--toplevel/vernacentries.ml78
11 files changed, 98 insertions, 119 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 1a67a37d7..bd5890e29 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -379,7 +379,6 @@ type vernac_expr =
| VernacBackTo of int
(* Commands *)
- | VernacDeclareTacticDefinition of tacdef_body list
| VernacCreateHintDb of string * bool
| VernacRemoveHints of string list * reference list
| VernacHints of obsolete_locality * string list * hints_expr
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0ad39d804..8d7b6a2b4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -751,11 +751,7 @@ GEXTEND Gram
GLOBAL: command query_command class_rawexpr;
command:
- [ [ IDENT "Ltac";
- l = LIST1 tacdef_body SEP "with" ->
- VernacDeclareTacticDefinition l
-
- | IDENT "Comments"; l = LIST0 comment -> VernacComments l
+ [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
(* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
| IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9c2f09db8..c7cb62d59 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -364,9 +364,6 @@ module Tactic =
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
- (* For Ltac definition *)
- let tacdef_body = Gram.entry_create "tactic:tacdef_body"
-
end
module Vernac_ =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7410d4e44..35973a4d7 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -229,7 +229,6 @@ module Tactic :
val binder_tactic : raw_tactic_expr Gram.entry
val tactic : raw_tactic_expr Gram.entry
val tactic_eoi : raw_tactic_expr Gram.entry
- val tacdef_body : Vernacexpr.tacdef_body Gram.entry
end
module Vernac_ :
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index edd32e833..c1f5e122b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -995,29 +995,6 @@ module Make
return (keyword "Cd" ++ pr_opt qs s)
(* Commands *)
- | VernacDeclareTacticDefinition l ->
- let pr_tac_body tacdef_body =
- let id, redef, body =
- match tacdef_body with
- | TacticDefinition ((_,id), body) -> pr_id id, false, body
- | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
- in
- let idl, body =
- match body with
- | Tacexpr.TacFun (idl,b) -> idl,b
- | _ -> [], body in
- id ++
- prlist (function None -> str " _"
- | Some id -> spc () ++ pr_id id) idl
- ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
- pr_raw_tactic body
- in
- return (
- hov 1
- (keyword "Ltac" ++ spc () ++
- prlist_with_sep (fun () ->
- fnl() ++ keyword "with" ++ spc ()) pr_tac_body l)
- )
| VernacCreateHintDb (dbname,b) ->
return (
hov 1 (keyword "Create HintDb" ++ spc () ++
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index e83313aa8..2d2ea1f8b 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -694,7 +694,6 @@ let rec tmpp v loc =
| VernacBackTo _ -> PCData "VernacBackTo"
(* Commands *)
- | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
| VernacCreateHintDb _ as x -> xmlTODO loc x
| VernacRemoveHints _ as x -> xmlTODO loc x
| VernacHints _ as x -> xmlTODO loc x
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 41b753fb8..ecaf0fb7c 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -173,13 +173,6 @@ let rec classify_vernac e =
| VernacRegister _
| VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
- | VernacDeclareTacticDefinition l ->
- let open Libnames in
- let open Vernacexpr in
- VtSideff (List.map (function
- | TacticDefinition ((_,r),_) -> r
- | TacticRedefinition (Ident (_,r),_) -> r
- | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
(* Who knows *)
| VernacLoad _ -> VtSideff [], VtNow
(* (Local) Notations have to disappear *)
diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4
index d75073877..f46a67008 100644
--- a/tactics/g_ltac.ml4
+++ b/tactics/g_ltac.ml4
@@ -48,6 +48,7 @@ let new_entry name =
e
let selector = new_entry "vernac:selector"
+let tacdef_body = new_entry "tactic:tacdef_body"
(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
proof editing and changes nothing else). Then sets it as the default proof mode. *)
@@ -311,6 +312,7 @@ open Constrarg
open Vernacexpr
open Vernac_classifier
open Goptions
+open Libnames
let print_info_trace = ref None
@@ -409,3 +411,19 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
| [ "Print" "Ltac" reference(r) ] ->
[ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
END
+
+VERNAC ARGUMENT EXTEND ltac_tacdef_body
+| [ tacdef_body(t) ] -> [ t ]
+END
+
+VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
+| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
+ VtSideff (List.map (function
+ | TacticDefinition ((_,r),_) -> r
+ | TacticRedefinition (Ident (_,r),_) -> r
+ | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
+ ] -> [
+ let lc = Locality.LocalityFixme.consume () in
+ Tacentries.register_ltac (Locality.make_module_locality lc) l
+ ]
+END
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index e40f5f46a..711cd8d9d 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Pp
open Errors
open Util
open Names
@@ -14,6 +15,8 @@ open Pcoq
open Egramml
open Egramcoq
open Vernacexpr
+open Libnames
+open Nameops
(**********************************************************************)
(* Tactic Notation *)
@@ -184,3 +187,77 @@ let add_ml_tactic_notation name prods =
} in
Lib.add_anonymous_leaf (inMLTacticGrammar obj);
extend_atomic_tactic name prods
+
+(** Command *)
+
+
+type tacdef_kind =
+ | NewTac of Id.t
+ | UpdateTac of Nametab.ltac_constant
+
+let is_defined_tac kn =
+ try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
+
+let register_ltac local tacl =
+ let map tactic_body =
+ match tactic_body with
+ | TacticDefinition ((loc,id), body) ->
+ let kn = Lib.make_kn id in
+ let id_pp = pr_id id in
+ let () = if is_defined_tac kn then
+ Errors.user_err_loc (loc, "",
+ str "There is already an Ltac named " ++ id_pp ++ str".")
+ in
+ let is_primitive =
+ try
+ match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
+ | Tacexpr.TacArg _ -> false
+ | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
+ with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+ in
+ let () = if is_primitive then
+ msg_warning (str "The Ltac name " ++ id_pp ++
+ str " may be unusable because of a conflict with a notation.")
+ in
+ NewTac id, body
+ | TacticRedefinition (ident, body) ->
+ let loc = loc_of_reference ident in
+ let kn =
+ try Nametab.locate_tactic (snd (qualid_of_reference ident))
+ with Not_found ->
+ Errors.user_err_loc (loc, "",
+ str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+ in
+ UpdateTac kn, body
+ in
+ let rfun = List.map map tacl in
+ let recvars =
+ let fold accu (op, _) = match op with
+ | UpdateTac _ -> accu
+ | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
+ in
+ List.fold_left fold [] rfun
+ in
+ let ist = Tacintern.make_empty_glob_sign () in
+ let map (name, body) =
+ let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
+ (name, body)
+ in
+ let defs () =
+ (** Register locally the tactic to handle recursivity. This function affects
+ the whole environment, so that we transactify it afterwards. *)
+ let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
+ let () = List.iter iter_rec recvars in
+ List.map map rfun
+ in
+ let defs = Future.transactify defs () in
+ let iter (def, tac) = match def with
+ | NewTac id ->
+ Tacenv.register_ltac false local id tac;
+ Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
+ | UpdateTac kn ->
+ Tacenv.redefine_ltac local kn tac;
+ let name = Nametab.shortest_qualid_of_tactic kn in
+ Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
+ in
+ List.iter iter defs
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 635415b9d..3cf0bc5cc 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -17,3 +17,5 @@ val add_tactic_notation :
val add_ml_tactic_notation : ml_tactic_name ->
Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
+
+val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d0af1b951..bbfa8818b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -914,81 +914,6 @@ let vernac_restore_state file =
(************)
(* Commands *)
-type tacdef_kind =
- | NewTac of Id.t
- | UpdateTac of Nametab.ltac_constant
-
-let is_defined_tac kn =
- try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
-
-let register_ltac local tacl =
- let map tactic_body =
- match tactic_body with
- | TacticDefinition ((loc,id), body) ->
- let kn = Lib.make_kn id in
- let id_pp = pr_id id in
- let () = if is_defined_tac kn then
- Errors.user_err_loc (loc, "",
- str "There is already an Ltac named " ++ id_pp ++ str".")
- in
- let is_primitive =
- try
- match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
- | Tacexpr.TacArg _ -> false
- | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
- with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
- in
- let () = if is_primitive then
- msg_warning (str "The Ltac name " ++ id_pp ++
- str " may be unusable because of a conflict with a notation.")
- in
- NewTac id, body
- | TacticRedefinition (ident, body) ->
- let loc = loc_of_reference ident in
- let kn =
- try Nametab.locate_tactic (snd (qualid_of_reference ident))
- with Not_found ->
- Errors.user_err_loc (loc, "",
- str "There is no Ltac named " ++ pr_reference ident ++ str ".")
- in
- UpdateTac kn, body
- in
- let rfun = List.map map tacl in
- let recvars =
- let fold accu (op, _) = match op with
- | UpdateTac _ -> accu
- | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
- in
- List.fold_left fold [] rfun
- in
- let ist = Tacintern.make_empty_glob_sign () in
- let map (name, body) =
- let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
- (name, body)
- in
- let defs () =
- (** Register locally the tactic to handle recursivity. This function affects
- the whole environment, so that we transactify it afterwards. *)
- let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
- let () = List.iter iter_rec recvars in
- List.map map rfun
- in
- let defs = Future.transactify defs () in
- let iter (def, tac) = match def with
- | NewTac id ->
- Tacenv.register_ltac false local id tac;
- Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
- | UpdateTac kn ->
- Tacenv.redefine_ltac local kn tac;
- let name = Nametab.shortest_qualid_of_tactic kn in
- Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
- in
- List.iter iter defs
-
-let vernac_declare_tactic_definition locality def =
- let local = make_module_locality locality in
- register_ltac local def
-
let vernac_create_hintdb locality id b =
let local = make_module_locality locality in
Hints.create_hint_db local id full_transparent_state b
@@ -1898,8 +1823,6 @@ let interp ?proof ~loc locality poly c =
| VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
(* Commands *)
- | VernacDeclareTacticDefinition def ->
- vernac_declare_tactic_definition locality def
| VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
| VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
| VernacHints (local,dbnames,hints) ->
@@ -1982,7 +1905,6 @@ let check_vernac_supports_locality c l =
| VernacCoercion _ | VernacIdentityCoercion _
| VernacInstance _ | VernacDeclareInstances _
| VernacDeclareMLModule _
- | VernacDeclareTacticDefinition _
| VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
| VernacSyntacticDefinition _
| VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 07:20:36 +0000