From 94affd965c1554d2ad10654e9832fcdb2a024daf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Apr 2009 13:55:46 +0000
Subject: - Fixed a little bug in previous commit (bad failure in case of
 unknown entry). - Added support for list of intropattern in Tactic Notation.

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

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 09b76d3f37..d085584264 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -47,7 +47,7 @@ let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, nt, po) ->
       let sep = match po with Some (_,sep) -> sep | _ -> "" in
-      let (etyp, e) = interp_entry_name (Some lev) nt sep in
+      let (etyp, e) = interp_entry_name true (Some lev) nt sep in
       GramNonTerminal (loc, etyp, e, Option.map fst po)
 
 let make_terminal_status = function
-- 
cgit v1.2.3