fixed intro.

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 2f72b23fa4c17ab775ee87df7469ca3578096290..238eb93673f6f46830c3f6784d32e187f479e0fb 100644 (file)
--- 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 ->