X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=3d7699ecde14207b2d3e7ad4410321d927f1076a;hb=72e4059f7141d5cdf573e470e9858a0e68d6fceb;hp=78d1bf181c8b99c1d14b965244eac25eacc7ebc0;hpb=d5e420ba0286d6b6ccab7101bdd75a1442385e06;p=helm.git

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 [