diff options
| author | herbelin | 2004-02-12 19:35:23 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-12 19:35:23 +0000 |
| commit | b847fcc99e35a09b862aa758c5e3f0b08a93202d (patch) | |
| tree | a1e88a9123be5255852cc93015fd5b22699633d6 /parsing | |
| parent | dabb8781bf86fb7f85aa4c96928252c6afc8f3cc (diff) | |
Localisation des erreurs d'internalisation des notations de tactiques
dans le module de leur définition.
Error_in_file dans Util et étendu avec possibilité de noms de modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egrammar.ml | 3 | ||||
| -rw-r--r-- | parsing/egrammar.mli | 5 |
2 files changed, 6 insertions, 2 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 5880c0263b..25333b6848 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -26,7 +26,8 @@ type all_grammar_command = int list option) | Grammar of grammar_command | TacticGrammar of - (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) + (string * (string * grammar_production list) * + (Names.dir_path * Tacexpr.raw_tactic_expr)) list let subst_all_grammar_command subst = function diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e1f4dc6b10..47b8beced3 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -22,7 +22,10 @@ type all_grammar_command = (int * Gramext.g_assoc option * notation * prod_item list * int list option) | Grammar of grammar_command - | TacticGrammar of (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list + | TacticGrammar of + (string * (string * grammar_production list) * + (Names.dir_path * Tacexpr.raw_tactic_expr)) + list val extend_grammar : all_grammar_command -> unit |