diff options
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 20bcb84a75..a3006e99cc 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -118,7 +118,7 @@ let is_applied_rewrite_relation env sigma rels t = let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in let _ = Typeclasses.resolve_one_typeclass env' evd inst in Some (it_mkProd_or_LetIn t rels) - with _ -> None) + with e when Errors.noncritical e -> None) | _ -> None let _ = @@ -218,7 +218,7 @@ let cstrevars evars = snd evars let evd_convertible env evd x y = try ignore(Evarconv.the_conv_x env x y evd); true - with _ -> false + with e when Errors.noncritical e -> false let rec decompose_app_rel env evd t = match kind_of_term t with @@ -1040,7 +1040,8 @@ module Strategies = let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1048,7 +1049,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None let fold_glob c : strategy = fun env avoid t ty cstr evars -> @@ -1056,7 +1057,8 @@ module Strategies = let sigma, c = Pretyping.understand_tcc (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1064,7 +1066,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None end @@ -1306,7 +1308,7 @@ let cl_rewrite_clause_newtac ?abs strat clause = let newtactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () - with e -> Proofview.tclZERO e + with e when Errors.noncritical e -> Proofview.tclZERO e let tactic_init_setoid () = init_setoid (); tclIDTAC @@ -1979,7 +1981,7 @@ let setoid_proof gl ty fn fallback = let evm = project gl in let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in fn env evm car rel gl - with e -> + with e when Errors.noncritical e -> try fallback gl with Hipattern.NoEquationFound -> let e = Errors.push e in |