* PRE_EVAL(dbd) *)
val index_constant:
dbd:Mysql.dbd ->
- owner:string ->
uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term ->
unit
* PRE_EVAL(dbd) *)
val index_inductive_def:
dbd:Mysql.dbd ->
- owner:string ->
uri:UriManager.uri -> types:Cic.inductiveType list ->
unit
(* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
- (** remove from the db all metadata pertaining to a given owner *)
-val clean: dbd:Mysql.dbd -> unit
+ (** remove from the db all metadata pertaining to a given owner
+ * @return list of uris removed from the db *)
+val clean: dbd:Mysql.dbd -> string list
+
+val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit