type flags = {
maxwidth: int;
+ maxsize: int;
maxdepth: int;
+ maxgoalsizefactor : int;
timeout: float;
use_library: bool;
use_paramod: bool;
(* (metasenv, subst, (metano,depth)list *)
type sort = P | T;;
type and_elem =
- Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list
+ (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list
type auto_result =
| Fail of string
- | Success of Cic.metasenv * Cic.substitution * and_elem list
+ | Success of (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * and_elem list