*)
(** index a Cic.Constant object and insert resulting metadata into the db
- * PRE_EVAL(dbh) *)
+ * PRE_EVAL(dbd) *)
val index_constant:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
owner:string ->
uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term ->
unit
(** index a Cic.InductiveDefinition object and insert resulting metadata into
* the db
- * PRE_EVAL(dbh) *)
+ * PRE_EVAL(dbd) *)
val index_inductive_def:
- dbh:Dbi.connection ->
+ 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: dbh:Dbi.connection -> owner:string -> unit
+val clean: dbd:Mysql.dbd -> owner:string -> unit