From d0f6d02f8ca0d6366b39e611518f0cc744282240 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 16:32:20 +0000
Subject: [PATCH] added syntax for letin

---
 helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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 [
-- 
2.39.2