syntax changes: "." at the end of the phrase instead of ";;"

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 1b1d690bdff2ca449fa26637d81f5ab4e7d10218..00b4c4418cf7847d82b8dcee13dfb1c6b00e97d3 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -344,7 +344,7 @@ EXTEND
         return_tactic loc (TacticAst.Transitivity t)
     ]
   ];
-  tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ];
+  tactical0: [ [ t = tactical; SYMBOL "." -> return_tactical loc t ] ];
   tactical:
     [ "command" NONA
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
@@ -438,6 +438,10 @@ EXTEND
         return_command loc (TacticAst.Baseuri uri)
     | [ IDENT "check"   | IDENT "Check" ]; t = term ->
         return_command loc (TacticAst.Check t)
+(*
+    | [ IDENT "alias"   | IDENT "Alias" ]; spec = alias_spec ->
+        return_command loc (TacticAst.Alias spec)
+*)
     ]
   ];
   script_entry: [