diff options
| author | Pierre-Marie Pédrot | 2014-08-18 01:25:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-18 01:28:19 +0200 |
| commit | 4b7de15309da63b30f53325383ead7004b1f2c26 (patch) | |
| tree | f49e277bb60a50bd8421ae86093acd23dde66904 /parsing | |
| parent | 243ffa4b928486122075762da6ce8da707e07daf (diff) | |
Moving the TacAlias node out of atomic tactics.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index c56a5a7004..f47eb1c091 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -274,7 +274,7 @@ let head_is_ident tg = match tg.tacgram_prods with let add_tactic_entry kn tg = let entry, pos = get_tactic_entry tg.tacgram_level in - let mkact loc l = (TacAtom(loc, TacAlias (loc,kn,l)):raw_tactic_expr) in + let mkact loc l = (TacAlias (loc,kn,l):raw_tactic_expr) in let () = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then error "Notation for simple tactic must start with an identifier." |