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 /printing/pptactic.ml | |
| 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 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 4cb7e9fb38..50a543968a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1201,7 +1201,7 @@ module Make | TacML (loc,s,l) -> pr_with_comments loc (pr.pr_extend 1 s l), lcall | TacAlias (loc,kn,l) -> - pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom + pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm |