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 b7cace0cb1dece3d5f54ae179acd9d251a39a7a5..356c0a369e7b286aea1d00d92ab790e6aa99a714 100644 (file)
--- 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???????";