diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-21 18:34:30 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-21 18:34:30 +0000 |
| commit | 8ea95ff47dcbad4f28a37dfd40882f4c83bcc49c (patch) | |
| tree | 4b68d679e28e462de1fb06fb0c09f94b8cc03c74 /tactics | |
| parent | 7a9708cd03e40bd9becb68d8e702be65d4992819 (diff) | |
Lazier behaviour of [auto] when introducing hypothesis: query the hint db's only when necessary. Hopefully should speed up [auto] a little.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -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 |