try
let ty' = unfold context ty in
if is_an_equality ty' then Some(t,ty') else None
try
let ty' = unfold context ty in
if is_an_equality ty' then Some(t,ty') else None
| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
| D ((n,_,P) as g)::tl ->
(match calculate_goal_ty g subst menv with
| None -> no_progress variant tl
| D ((n,_,P) as g)::tl ->
(match calculate_goal_ty g subst menv with
| None -> no_progress variant tl
| (m, s, _, _, [],_)::orlist ->
(* complete success *)
Proved (m, s, orlist, tables, cache, maxm)
| (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 ->
(* 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)
(* 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 ->
(debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
aux tables maxm flags cache orlist)
else if prunable_for_size flags s m todo then
(debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
aux tables maxm flags cache orlist)
else if prunable_for_size flags s m todo then
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 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
AutoTypes.close_more = close_more;
AutoTypes.dont_cache_failures = false;
AutoTypes.maxgoalsizefactor = gsize;
AutoTypes.close_more = close_more;
AutoTypes.dont_cache_failures = false;
AutoTypes.maxgoalsizefactor = gsize;
in
match auto_main tables newmeta context flags universe cache [elem] with
| Proved (metasenv,subst,_, tables,cache,_) ->
in
match auto_main tables newmeta context flags universe cache [elem] with
| Proved (metasenv,subst,_, tables,cache,_) ->
(* we take the whole universe (no signature filtering) *)
init_cache_and_tables false true false true universe (proof,goal)
in
(* we take the whole universe (no signature filtering) *)
init_cache_and_tables false true false true universe (proof,goal)
in
let table =
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
init_cache_and_tables
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
init_cache_and_tables