(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+ val mqi_handle : MQIConn.handle
+ val dbd:Mysql.dbd
end
;;
val whd_in_scratch : unit -> unit
val reduce_in_scratch : unit -> unit
val simpl_in_scratch : unit -> unit
+ val auto : unit -> unit
end
module Make (C: Callbacks) : Tactics =
in
handle_refresh_exception
(fun () ->
- let metasenv',expr =
+ let metasenv',expr,ugraph = (*TASSI: FIX THIS*)
(match term with
| None -> ()
| Some t -> (C.term_editor ())#set_term t);
List.find (function (m,_,_) -> m=metano) metasenv
in
canonical_context in
- let (metasenv',expr) =
+ let (metasenv',expr,ugraph) =(* FIX THIS AND *)
(C.term_editor ())#get_metasenv_and_term
canonical_context metasenv
in
| _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
+
let intros =
call_tactic
(ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
let exact = call_tactic_with_input ProofEngine.exact
let apply = call_tactic_with_input ProofEngine.apply
+ let auto = call_tactic (ProofEngine.auto ~dbd:C.dbd)
let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
let elimtype = call_tactic_with_input ProofEngine.elim_type
let whd = call_tactic_with_goal_inputs ProofEngine.whd