diff options
| author | Pierre-Marie Pédrot | 2015-12-31 13:56:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-02 02:02:02 +0100 |
| commit | f3e611b2115b425f875e971ac9ff7534c2af2800 (patch) | |
| tree | d153ca5e2205efe2ea76f5bdf05d967df80c3736 /parsing | |
| parent | d5b1807e65f7ea29d435c3f894aa551370c5989f (diff) | |
Separation of concern in TacAlias API.
The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 2bc5b0f83f..bd9bacbc60 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -286,9 +286,9 @@ let add_tactic_entry kn tg = (** HACK to handle especially the tactic(...) entry *) let wit = Genarg.rawwit Constrarg.wit_tactic in if Genarg.argument_type_eq t (Genarg.unquote wit) then - (id, Tacexp (Genarg.out_gen wit arg)) + Tacexp (Genarg.out_gen wit arg) else - (id, TacGeneric arg) + TacGeneric arg in let l = List.map2 map l types in (TacAlias (loc,kn,l):raw_tactic_expr) |