diff options
| author | Hugo Herbelin | 2014-08-17 19:26:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:39 +0200 |
| commit | 924771d6fdd1349955c2d0f500ccf34c2109507b (patch) | |
| tree | 1bb75c17f846a185c88bcd332e5890ebb2c41076 /tactics | |
| parent | e8a531dfa623e3badc3baddcf13f0a7975c37886 (diff) | |
Improving error message when applying rewrite to an expression which is not an equality.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 1 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 |
3 files changed, 3 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 061d8ca703..beb0cfae8f 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 ca7fb7b0a8..9102b244c5 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 662d02a93e..8260da9d71 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 |