diff options
| author | ppedrot | 2013-07-02 17:28:22 +0000 |
|---|---|---|
| committer | ppedrot | 2013-07-02 17:28:22 +0000 |
| commit | 556c2ce6f1b09d09484cc83f6ada213496add45b (patch) | |
| tree | fe48802a1c5876c42c9ed03dbb6d876030bf2aac /grammar | |
| parent | 89abe2a141b3baa11bf0e8bcdecaf68220251c6e (diff) | |
Removing the use of leveled tactics wit_tacticn. It is now handled
through a unique generic argument, and the level is only considered
at parsing time.
This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/grammar.mllib | 1 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index f361bee492..bde5c15f3f 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -31,7 +31,6 @@ Stdarg Constrarg Tok Lexer -Extrawit Pcoq Q_util Q_coqast diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 1b29da6813..d494a92d88 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -15,7 +15,6 @@ open Q_util open Q_coqast open Argextend open Pcoq -open Extrawit open Egramml open Compat |