diff options
| author | Pierre-Marie Pédrot | 2014-12-16 14:33:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-12-16 14:38:51 +0100 |
| commit | f88cce2698da000ab9054da31330db70997a41a4 (patch) | |
| tree | 8bc74094c06411792ff1431c4ce73c77ec94bb2f /tactics | |
| parent | 5ba84979df97996cd04f44e506742bb58ecf0465 (diff) | |
Fixing CAMLP4 compilation.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 11 |
3 files changed, 10 insertions, 7 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 4f23e35204..dfb3def564 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 3905708172..2150042a5a 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 d65177c5cd..d6f2f2cdd3 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 |