From 43a42296efbcb298037448e000280efb0e26e368 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 4 Mar 2003 13:56:22 +0000
Subject: Bug délimiteur de scope en vieil affichage ast

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

diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index c506c1ff25..cc4e60d43f 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -187,7 +187,7 @@ let pr_parenthesis inherited se strm =
 let print_delimiters inh se strm = function
   | None -> pr_parenthesis inh se strm
   | Some key ->
-      let left = "`"^key^":" and right = "`" in
+      let left = "'"^key^":" and right = "'" in
       let lspace =
 	if is_letter (left.[String.length left -1]) then str " " else mt () in
       let rspace =
@@ -241,7 +241,7 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
 	  | Some (scopt,key) ->
 	      print_delimiters inherited se
 		(print_syntax_entry rec_pr (option_cons scopt scopes) env 
-		  {se with syn_hunks = [sub]}) scopt)
+		  {se with syn_hunks = [sub]}) key)
     | _ ->
 	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
   )
-- 
cgit v1.2.3