type status = {
aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ moo_content_rev: string list; (*CSC: a TacticAst.command list would be better *)
proof_status: proof_status;
options: options;
objects: (UriManager.uri * string) list;
with Failure _ ->
command_error (sprintf "Not an integer value \"%s\"" value))
in
- { status with options = StringMap.add name value status.options }
+ if StringMap.mem name status.options && name = "baseuri" then
+ command_error "Redefinition of 'baseuri' is forbidden."
+ else
+ { status with options = StringMap.add name value status.options }
(* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
class type console =