From 87229783dd5ad20e16129f577efb1f94358231ac Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 2 Nov 2006 13:59:14 +0000
Subject: gestion speciale du niveau 5 des ltac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 18ff746f1c..eaa750ab3d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -112,6 +112,8 @@ let print_grammar univ = function
   | "tactic" -> 
       msgnl (str "Entry tactic_expr is");
       Gram.Entry.print Pcoq.Tactic.tactic_expr;
+      msgnl (str "Entry binder_tactic is");
+      Gram.Entry.print Pcoq.Tactic.binder_tactic;
       msgnl (str "Entry simple_tactic is");
       Gram.Entry.print Pcoq.Tactic.simple_tactic;
   | "vernac" -> 
-- 
cgit v1.2.3