diff options
| -rw-r--r-- | intf/vernacexpr.mli | 6 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 20 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 9 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 63 |
6 files changed, 57 insertions, 49 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 0e659459e..07a206b53 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -386,7 +386,7 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of (reference * bool * raw_tactic_expr) list + | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr @@ -453,6 +453,10 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr +and tacdef_body = + | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + and located_vernac_expr = Loc.t * vernac_expr (* A vernac classifier has to tell if a command: diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 4a9ca23f1..181c2395d 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -242,17 +242,17 @@ GEXTEND Gram | n = integer -> MsgInt n ] ] ; - ltac_def_kind: - [ [ ":=" -> false - | "::=" -> true ] ] - ; - (* Definitions for tactics *) - tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - (name, redef, body) ] ] + tacdef_body: + [ [ id = ident; it=LIST1 input_fun; ":="; body = tactic_expr -> + Vernacexpr.TacticDefinition ((!@loc,id), TacFun (it, body)) + | name = Constr.global; it=LIST1 input_fun; "::="; body = tactic_expr -> + Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + | id = ident; ":="; body = tactic_expr -> + Vernacexpr.TacticDefinition ((!@loc,id), body) + | name = Constr.global; "::="; body = tactic_expr -> + Vernacexpr.TacticRedefinition (name, body) + ] ] ; tactic: [ [ tac = tactic_expr -> tac ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ad4d9e501..fdba41385 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -237,7 +237,7 @@ 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 : (reference * bool * 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 5110cf7b2..f216c599d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1031,12 +1031,17 @@ module Make (* Commands *) | VernacDeclareTacticDefinition l -> - let pr_tac_body (id, redef, body) = + let pr_tac_body tacdef_body = + let id, redef, body = + match tacdef_body with + | TacticDefinition ((_,id), body) -> str (Id.to_string 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 - pr_ltac_ref id ++ + id ++ prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 90490c38b..58e26de84 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -177,9 +177,11 @@ let rec classify_vernac e = | VernacComments _ -> VtSideff [], VtLater | VernacDeclareTacticDefinition l -> let open Libnames in + let open Vernacexpr in VtSideff (List.map (function - | (Ident (_,r),_,_) -> r - | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater + | 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/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 010a0afe4..28b5bace1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -942,40 +942,37 @@ type tacdef_kind = let is_defined_tac kn = try ignore (Tacenv.interp_ltac kn); true with Not_found -> false -let make_absolute_name ident repl = - let loc = loc_of_reference ident in - if repl then - 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 - else - let id = Constrexpr_ops.coerce_reference_to_id ident in - let kn = Lib.make_kn id in - let () = if is_defined_tac kn then - Errors.user_err_loc (loc, "", - str "There is already an Ltac named " ++ pr_reference ident ++ 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 " ++ pr_reference ident ++ - str " may be unusable because of a conflict with a notation.") - in - NewTac id - let register_ltac local tacl = - let map (ident, repl, body) = - let name = make_absolute_name ident repl in - (name, body) + let map tactic_body = + match tactic_body with + | TacticDefinition ((loc,id), body) -> + let kn = Lib.make_kn id in + let id_pp = str (Id.to_string 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 = |