diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-09 02:48:07 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-09 02:48:07 +0000 |
| commit | 485ab2c54051b3c9127477956002956971d41e3b (patch) | |
| tree | 2d32ac92804101a7aaf96c10e32158ccddc0558e /printing/pptactic.ml | |
| parent | 84388f06b9385b8c194718635ac593083449c4dd (diff) | |
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
Instead of putting the body directly in the AST, we register it in a table.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2ce3eba06..0bb9982c2 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -623,7 +623,7 @@ let rec pr_atom0 = function and pr_atom1 = function | TacExtend (loc,s,l) -> pr_with_comments loc (pr_extend 1 s l) - | TacAlias (loc,s,l,_) -> + | TacAlias (loc,s,l) -> pr_with_comments loc (pr_extend 1 s (List.map snd l)) (* Basic tactics *) @@ -912,7 +912,7 @@ let rec pr_tac inherited tac = pr_tac (lcomplete,E) t, lcomplete | TacId l -> str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom - | TacAtom (loc,TacAlias (_,s,l,_)) -> + | TacAtom (loc,TacAlias (_,s,l)) -> pr_with_comments loc (pr_extend (level_of inherited) s (List.map snd l)), latom |