diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 14:46:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 14:46:43 +0000 |
| commit | a29edb0a5e9d420a3780a7034aad4ef9cfe7c148 (patch) | |
| tree | 9b2ec00ba7d5a91491645c41cc41ab4f2bd07f1a /tactics/tacinterp.mli | |
| parent | 5dcc913519b8822ddf59eb3a356028f45f42cc3b (diff) | |
New cleaning phase of the Local/Global option management
- Clarification and documentation of the different styles of
Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 18873d1c6..238a329fd 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -67,7 +67,8 @@ val get_debug : unit -> debug_info (* Adds a definition for tactics in the table *) val add_tacdef : - bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit + Vernacexpr.locality_flag -> bool -> + (Libnames.reference * bool * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit (* Tactic extensions *) |