From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 21 Jan 2005 09:35:33 +0000 (+0000)
Subject: syntax changes: "." at the end of the phrase instead of ";;"
X-Git-Tag: V_0_1_0~103
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebc6741574ced219ad51e912b947c96e1d470772;p=helm.git

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 1b1d690bd..00b4c4418 100644
--- 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: [