From 21fac7762b3376d0c7d2eee4066aae9ce7268ba8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 1 Jun 2005 11:04:22 +0000
Subject: [PATCH] fixed intro.

---
 helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 2f72b23fa..238eb9367 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -373,7 +373,7 @@ EXTEND
         let idents = match idents with None -> [] | Some idents -> idents in
         TacticAst.Intros (loc, num, idents)
     | [ IDENT "intro" ] ->
-        TacticAst.Intros (loc, None, [])
+        TacticAst.Intros (loc, Some 1, [])
     | [ IDENT "left" ] -> TacticAst.Left loc
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
-- 
2.39.2