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 | |
| 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')
| -rw-r--r-- | parsing/egramcoq.ml | 5 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 1 |
2 files changed, 4 insertions, 2 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 669370890..34e0dcdef 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -249,6 +249,7 @@ type tactic_grammar = { tacgram_key : string; tacgram_level : int; tacgram_prods : grammar_prod_item list; + tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr; } type all_grammar_command = @@ -268,12 +269,12 @@ let add_tactic_entry tg = if not (head_is_ident tg) then error "Notation for simple tactic must start with an identifier."; let mkact loc l = - (TacAlias (loc,tg.tacgram_key,l):raw_atomic_tactic_expr) in + (TacAlias (loc,tg.tacgram_key,l,tg.tacgram_tactic):raw_atomic_tactic_expr) in make_rule mkact tg.tacgram_prods end else let mkact loc l = - (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l)):raw_tactic_expr) in + (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l,tg.tacgram_tactic)):raw_tactic_expr) in make_rule mkact tg.tacgram_prods in synchronize_level_positions (); grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]); 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} *) |