-type ng_status =
- | ProofMode of NTacStatus.tac_status
- | CommandMode of NEstatus.status
-
-class status =
- fun (mcr : GrafiteMarshal.moo) (ps : proof_status) (o : UriManager.uri list)
- (c : CoercDb.coerc_db) (ac : AutomationCache.cache) (b : string)
- (ns : ng_status)
- ->
+class status = fun (b : string) ->
+ let fake_obj =
+ NUri.uri_of_string "cic:/matita/dummy.decl",0,[],[],
+ NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular))
+ in