(* stops at the first solution *)
val auto:
- AutoTypes.universe ->
- AutoTypes.cache ->
+ HMysql.dbd ->
+ AutoCache.cache ->
Cic.context ->
Cic.metasenv ->
ProofEngineTypes.goal list -> (* goals in AND *)
AutoTypes.flags ->
- (Cic.substitution * Cic.metasenv) option * AutoTypes.cache
+ (Cic.substitution * Cic.metasenv) option * AutoCache.cache
val auto_all_solutions:
- AutoTypes.universe ->
- AutoTypes.cache ->
+ HMysql.dbd ->
+ AutoCache.cache ->
Cic.context ->
Cic.metasenv ->
ProofEngineTypes.goal list ->
AutoTypes.flags ->
- (Cic.substitution * Cic.metasenv) list * AutoTypes.cache
+ (Cic.substitution * Cic.metasenv) list * AutoCache.cache
+
+val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
+