try
let ty' = unfold context ty in
if is_an_equality ty' then Some(t,ty') else None
- with _ -> None) (* catturare l'eccezione giusta di unfold *)
+ with ProofEngineTypes.Fail _ -> None)
equations
in
let bag = Equality.mk_equality_bag () in
| (m, s, _, _, [],_)::orlist ->
(* complete success *)
Proved (m, s, orlist, tables, cache, maxm)
- | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
+ | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
+ when not flags.AutoTypes.do_types ->
(* skip since not Prop, don't even check if closed by side-effect *)
aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
| (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
(* timeout *)
debug_print (lazy ("FAIL: TIMEOUT"));
Gaveup (tables, cache, maxm)
- | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
+ | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
(* attack g *)
match calculate_goal_ty g s m with
| None ->
let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
+ let do_type = bool "type" false in
let timeout = int "timeout" 0 in
{ AutoTypes.maxdepth =
if use_only_paramod then 2 else depth;
AutoTypes.close_more = close_more;
AutoTypes.dont_cache_failures = false;
AutoTypes.maxgoalsizefactor = gsize;
+ AutoTypes.do_types = do_type;
}
let applyS_tac ~dbd ~term ~params ~universe =