From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 20 Jan 2005 10:24:44 +0000 (+0000)
Subject: added cmdline alias "command" for "tactica"
X-Git-Tag: V_0_1_0~121
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b118abe6e411f5e9ac6f7adc17de602bdf4a0830;p=helm.git

added cmdline alias "command" for "tactica"
---

diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml
index b7cace0cb..356c0a369 100644
--- a/helm/ocaml/cic_disambiguation/test_parser.ml
+++ b/helm/ocaml/cic_disambiguation/test_parser.ml
@@ -33,7 +33,7 @@ let mode =
     | "alias" -> prerr_endline "Alias"; `Alias
     | "term" -> prerr_endline "Term"; `Term
     | "tactic" -> prerr_endline "Tactic"; `Tactic
-    | "tactical" -> prerr_endline "Tactical"; `Tactical
+    | "tactical" | "command" -> prerr_endline "Tactical"; `Tactical
     | "script" -> prerr_endline "Script"; `Script
     | _ ->
         prerr_endline "What???????";