diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-09 07:08:59 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-09 07:08:59 +0000 |
| commit | 36e41e7581c86214a9f0f97436eb96a75b640834 (patch) | |
| tree | 2c99a4b163e976272c7931d0889611d8c13a15ae /parsing/egramcoq.mli | |
| parent | 485ab2c54051b3c9127477956002956971d41e3b (diff) | |
Revert the previous commit. It broke Coq compilation.
Tactics notation interpretation was messed up because of the use of
identical keys for different notations. All my tentative fixes were
unsuccessful, so better blankly revert the commit for now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/egramcoq.mli')
| -rw-r--r-- | parsing/egramcoq.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 5953eb0f8..9ae49f718 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -44,6 +44,7 @@ type tactic_grammar = { tacgram_key : string; tacgram_level : int; tacgram_prods : grammar_prod_item list; + tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr; } (** {5 Adding notations} *) |