From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 10 Sep 2009 14:41:47 +0000 (+0000)
Subject: allow @{ ... } as the identifier of the letin
X-Git-Tag: make_still_working~3484
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=09cfd99de377d72d7af96ad9815342a1b7b467a9;p=helm.git

allow @{ ... } as the identifier of the letin
---

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index af9edd9be..1a664d525 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -714,8 +714,8 @@ EXTEND
   [
     [ "let"; 
      var = 
-      [ LPAREN; id = IDENT; SYMBOL ":"; typ = term; RPAREN ->
-	  Ast.Ident(id,None), Some typ
+      [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
+	  id, Some typ
       | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
 	  Ast.Ident(id,None), ty ];
       SYMBOL <:unicode<def>> (* ≝ *);
@@ -816,6 +816,8 @@ let exc_located_wrapper f =
   with
   | Stdpp.Exc_located (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc, Parse_error msg))
+  | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
+      raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
   | Stdpp.Exc_located (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))