diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-25 18:33:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-25 18:53:02 +0200 |
| commit | d5f3727e0c218be41f0c5547677761fa7223e744 (patch) | |
| tree | 81886686d2f7c5b68971a46f6a12d5525b4f05f7 /plugins/cc | |
| parent | 43732086e664ff1fe59617a673e82cab6464c5e1 (diff) | |
Removing useless try-with clauses in Goal.enter variants.
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index f4f62cb85..ac148fe18 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -246,7 +246,6 @@ let _M =mkMeta let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_type_of gl in - try (* type_of can raise exceptions *) match p.p_rule with Ax c -> Proofview.V82.tactic (exact_check c) | SymAx c -> @@ -315,7 +314,6 @@ let rec proof_tac p : unit Proofview.tactic = let injt= mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = |