diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 9c153b15e..684329419 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -650,7 +650,7 @@ and my_find_search db_list local_db hdc concl = match t with | Res_pf (term,cl) -> unify_resolve (term,cl) | ERes_pf (_,c) -> (fun gl -> error "eres_pf") - | Give_exact c -> exact_no_check c + | Give_exact c -> exact_check c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_resolve (term,cl)) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 896218c80..5667796fe 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -31,8 +31,8 @@ open Rawterm let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 or occur_existential t2 then - tclTHEN (unify t1) (exact_no_check c) gl - else exact_no_check c gl + tclTHEN (unify t1) (exact_check c) gl + else exact_check c gl let assumption id = e_give_exact (mkVar id) |