diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-26 14:25:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-26 14:25:48 +0000 |
| commit | c8a8c52d313bfddf27660e0de2d7ffbf4658b87c (patch) | |
| tree | 8c94d099eade39beac72e991faebd571a0b7f7c5 /contrib | |
| parent | 85832c4d17c205644534f6ebb5cbe7c2053f9f9b (diff) | |
11715 continued
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11716 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/blast.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index ddedbb325..189c5360f 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -148,6 +148,8 @@ let pp_string x = (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) +let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l) + let unify_e_resolve (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false clenv' gls in @@ -192,9 +194,9 @@ and e_my_find_search db_list local_db hdc concl = | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> Auto.conclPattern concl p tacast in - (free_try tac,fmt_autotactic t)) + (free_try tac,pr_autotactic t)) (*i - fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); + fun gls -> pPNL (pr_autotactic t); Format.print_flush (); try tac gls with e when Logic.catchable_exception(e) -> (Format.print_string "Fail\n"; @@ -206,7 +208,7 @@ and e_my_find_search db_list local_db hdc concl = and e_trivial_resolve db_list local_db gl = try - Auto.priority + priority (e_my_find_search db_list local_db (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] |