From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 16:32:20 +0000 (+0000)
Subject: added syntax for letin
X-Git-Tag: PRE_INDEX_1~55
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d0f6d02f8ca0d6366b39e611518f0cc744282240;p=helm.git

added syntax for letin
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 78d1bf181..3d7699ecd 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -377,8 +377,8 @@ EXTEND
     | [ IDENT "intro" ] ->
         TacticAst.Intros (loc, Some 1, [])
     | [ IDENT "left" ] -> TacticAst.Left loc
-    | [ "let" | "Let" ];
-      t = tactic_term; "in"; where = IDENT ->
+    | [ IDENT "letin" ];
+       where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         TacticAst.LetIn (loc, t, where)
     | kind = reduction_kind;
       pat = OPT [