diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 3ba6b9f1b..92750094c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1008,14 +1008,14 @@ and decomp_and_register_decls p kont decls = exception Uplift of tactic list -let rec search_gen p n mod_delta db_list local_db = - let rec search n local_db gl = - if n=0 then error "BOUND 2"; - tclFIRST - (assumption :: - intros_decomp p (search n) [] local_db 1 :: - List.map (fun ntac -> tclTHEN ntac (search (n-1) local_db)) - (possible_resolve mod_delta db_list local_db (pf_concl gl))) gl +let search_gen p n mod_delta db_list local_db = + let rec search n local_db = + if n=0 then (fun gl -> error "BOUND 2") else + tclORELSE0 assumption + (tclORELSE0 (intros_decomp p (search n) [] local_db 1) + (fun gl -> tclFIRST + (List.map (fun ntac -> tclTHEN ntac (search (n-1) local_db)) + (possible_resolve mod_delta db_list local_db (pf_concl gl))) gl)) in search n local_db |