diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:51:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:51:59 +0000 |
| commit | 33a25f335839886cc205946bdc198ebab3b386de (patch) | |
| tree | 7d76954f046caa73ff9880c97af2fdb24854aaee /tactics | |
| parent | e75373c73188d8fbcf7578a0578ce27d60c7b73f (diff) | |
Option pour rendre les vérifications du refiner optionnelle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
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) |