@@ -35,9 +35,9 @@ help =
3535 ([":r",":reload"], NoArg, "Reload current file"),
3636 ([":l",":load"], FileArg, "Load a new file"),
3737 ([":cd"], FileArg, "Change working directory"),
38− ([":m",":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons
38+ ([":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons
3939 ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),
40− ([":m",":metavars"], MetaVarArg, "Show remaining proof obligations (metavariables)"),
40+ ([":m",":metavars"], NoArg, "Show remaining proof obligations (metavariables)"),
4141 ([":p",":prove"], MetaVarArg, "Prove a metavariable"),
4242 ([":a",":addproof"], NameArg, "Add proof to source file"),
4343 ([":rmproof"], NameArg, "Remove proof from proof stack"),