diff options
| author | aspiwack | 2013-11-02 15:41:07 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:41:07 +0000 |
| commit | 8c1e25acc561767980acdccc987087f51e0e2a12 (patch) | |
| tree | c7a22b8810a8f8f8d340683495e7452be5cf31df | |
| parent | f9106194333c11ab86460660f3603565ecd7785a (diff) | |
Tacticals.New.tclWITHHOLES: clean up.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17027 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacticals.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f25bae9bb8..fe527a811d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -512,7 +512,7 @@ module New = struct try Refiner.check_evars env new_sigma sigma initial_sigma; tclUNIT () - with e -> + with e when Errors.noncritical e -> tclZERO e in let check_evars_if = @@ -523,7 +523,7 @@ module New = struct else tclUNIT () in - Proofview.V82.tactic (Refiner.tclEVARS sigma) <*> tac x <*> check_evars_if + Proofview.V82.tclEVARS sigma <*> tac x <*> check_evars_if let tclTIMEOUT n t = Proofview.tclOR |