diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | parsing/compat.ml4 | 2 | ||||
| -rw-r--r-- | tactics/coretactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 11 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
7 files changed, 14 insertions, 11 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 25ce4cdaf..1d5bf2583 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -204,7 +204,7 @@ let declare_tactic loc s c cl = match cl with let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { - let obj () = Tacenv.register_ltac ~{for_ml=True} False $name$ $body$ in + let obj () = Tacenv.register_ltac True False $name$ $body$ in try do { Tacenv.register_ml_tactic $se$ $tac$; Mltop.declare_cache_obj obj $plugin_name$; } diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index ce0390e1d..4c63b95f5 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -221,7 +221,7 @@ end module GrammarMake (L:LexerSig) : GrammarSig = struct (* We need to refer to Coq's module Loc before it is hidden by include *) - let raise_coq_loc loc e = raise (Loc.add_loc e (to_coqloc loc)) + let raise_coq_loc loc e = Loc.raise (to_coqloc loc) e include Camlp4.Struct.Grammar.Static.Make (L) type 'a entry = 'a Entry.t type action = Action.t diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 4f23e3520..dfb3def56 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -205,7 +205,7 @@ let initial_atomic () = let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in let iter (s, t) = let body = TacAtom (dloc, t) in - Tacenv.register_ltac false (Id.of_string s) body + Tacenv.register_ltac false false (Id.of_string s) body in let () = List.iter iter [ "red", TacReduce(Red false,nocl); @@ -219,7 +219,7 @@ let initial_atomic () = "auto", TacAuto(Off,None,[],None); ] in - let iter (s, t) = Tacenv.register_ltac false (Id.of_string s) t in + let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in List.iter iter [ "idtac",TacId []; "fail", TacFail(ArgArg 0,[]); diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 390570817..2150042a5 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -121,7 +121,7 @@ let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj subst_function = subst_md; classify_function = classify_md} -let register_ltac ?(for_ml=false) local id tac = +let register_ltac for_ml local id tac = ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac))) let redefine_ltac local kn tac = diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index d65177c5c..d6f2f2cdd 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -25,10 +25,13 @@ val interp_alias : alias -> glob_tactic_expr (** {5 Coq tactic definitions} *) -val register_ltac : ?for_ml:bool -> bool -> Id.t -> glob_tactic_expr -> unit -(** Register a new Ltac with the given name and body. If the boolean flag is set - to true, then this is a local definition. It also puts the Ltac name in the - nametab, so that it can be used unqualified. *) +val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit +(** Register a new Ltac with the given name and body. + + The first boolean indicates whether this is done from ML side, rather than + Coq side. If the second boolean flag is set to true, then this is a local + definition. It also puts the Ltac name in the nametab, so that it can be + used unqualified. *) val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit (** Replace a Ltac with the given name and body. If the boolean flag is set diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 85f8f61a8..6d6376de3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -141,7 +141,7 @@ let extend_atomic_tactic name entries = | None -> () | Some args -> let body = Tacexpr.TacML (Loc.ghost, name, args) in - Tacenv.register_ltac false (Names.Id.of_string id) body + Tacenv.register_ltac false false (Names.Id.of_string id) body in List.iter add_atomic entries diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4a4c5a433..1b199d83c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -962,7 +962,7 @@ let register_ltac local isrec tacl = let defs = List.map map rfun in let iter (def, tac) = match def with | NewTac id -> - Tacenv.register_ltac local id tac; + 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; |