diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tacinterp.ml | 52 | ||||
-rw-r--r-- | tactics/tacinterp.mli | 2 |
2 files changed, 37 insertions, 17 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c9dee28d2..58d7e358c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2655,40 +2655,60 @@ let print_ltac id = errorlabstrm "print_ltac" (pr_qualid id ++ spc() ++ str "is not a user defined tactic") +open Libnames + (* Adds a definition for tactics in the table *) -let make_absolute_name (loc,id) repl = +let make_absolute_name ident repl = + let loc = loc_of_reference ident in try - let kn = if repl then Nametab.locate_tactic (make_short_qualid id) else Lib.make_kn id in + let id, kn = + if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident)) + else let id = Pcoq.coerce_global_to_id ident in + Some id, Lib.make_kn id + in if Gmap.mem kn !mactab then - if repl then kn + if repl then id, kn else user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is already an Ltac named " ++ pr_id id) + str "There is already an Ltac named " ++ pr_reference ident) else if is_atomic_kn kn then user_err_loc (loc,"Tacinterp.add_tacdef", - str "Reserved Ltac name " ++ pr_id id) - else kn + str "Reserved Ltac name " ++ pr_reference ident) + else id, kn with Not_found -> user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is no Ltac named " ++ pr_id id) + str "There is no Ltac named " ++ pr_reference ident) + +let rec filter_map f l = + let rec aux acc = function + [] -> acc + | hd :: tl -> + match f hd with + Some x -> aux (x :: acc) tl + | None -> aux acc tl + in aux [] l let add_tacdef isrec tacl = -(* let isrec = if !Flags.p1 then isrec else true in*) - let rfun = List.map (fun ((loc,id as locid),b,_) -> (id,make_absolute_name locid b)) tacl in + let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in let ist = - {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in + {(make_empty_glob_sign()) with ltacrecvars = + if isrec then filter_map + (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun + else []} in let gtacl = - List.map2 (fun ((_,id),b,def) (_, qid) -> - let k = if b then UpdateTac qid else NewTac id in + List.map2 (fun (_,b,def) (id, qid) -> + let k = if b then UpdateTac qid else NewTac (Option.get id) in let t = Flags.with_option strict_check (intern_tactic ist) def in (k, t)) tacl rfun in let id0 = fst (List.hd rfun) in - let _ = Lib.add_leaf id0 (inMD gtacl) in + let _ = match id0 with Some id0 -> ignore(Lib.add_leaf id0 (inMD gtacl)) + | _ -> Lib.add_anonymous_leaf (inMD gtacl) in List.iter - (fun ((_,id),b,_) -> - if b then Flags.if_verbose msgnl (pr_id id ++ str " is redefined") - else Flags.if_verbose msgnl (pr_id id ++ str " is defined")) + (fun (id,b,_) -> + Flags.if_verbose msgnl (Libnames.pr_reference id ++ + (if b then str " is redefined" + else str " is defined"))) tacl (***************************************************************************) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index db67d1473..2a490fdac 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -63,7 +63,7 @@ val get_debug : unit -> debug_info (* Adds a definition for tactics in the table *) val add_tacdef : - bool -> (identifier Util.located * bool * raw_tactic_expr) list -> unit + bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit (* Tactic extensions *) |