diff options
| -rw-r--r-- | proofs/refiner.ml | 13 | ||||
| -rw-r--r-- | tactics/equality.ml | 1 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 |
4 files changed, 11 insertions, 7 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 68fdea652..391a78b34 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -272,11 +272,14 @@ let ite_gen tcal tac_if continue tac_else gl= if !success then raise e else - tac_else gl in - try - tcal tac_if0 continue gl - with (* Breakpoint *) - | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl + try + tac_else gl + with + e' when Errors.noncritical e' -> raise e in + try + tcal tac_if0 continue gl + with (* Breakpoint *) + | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 061d8ca70..beb0cfae8 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1447,6 +1447,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let expected_goal = nf_betaiota sigma expected_goal in (* Retype to get universes right *) let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in + let sigma, _ = Typing.e_type_of env sigma body in sigma,body,expected_goal (* Like "replace" but decompose dependent equalities *) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index ca7fb7b0a..9102b244c 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1949,6 +1949,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let _, res = substrat (hypinfo, 0) env avoid t ty cstr evars in (), res in + init_setoid (); try tclWEAK_PROGRESS (tclTHEN @@ -1965,7 +1966,6 @@ let general_s_rewrite_clause x = | Some id -> general_s_rewrite (Some id) let general_s_rewrite_clause x y z w ~new_goals = - newtactic_init_setoid () <*> Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals) let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 662d02a93..8260da9d7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -379,7 +379,7 @@ module New = struct tclINDEPENDENT begin tclIFCATCH t1 (fun () -> t2) - (fun _ -> t3) + (fun e -> Proofview.tclORELSE t3 (fun e' -> tclZERO e)) end let tclIFTHENSVELSE t1 a t3 = tclIFCATCH t1 |