From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 1 Jun 2005 11:04:22 +0000 (+0000)
Subject: fixed intro.
X-Git-Tag: PRE_INDEX_1~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=21fac7762b3376d0c7d2eee4066aae9ce7268ba8;p=helm.git

fixed intro.
---

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