diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-17 19:26:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:39 +0200 |
| commit | 924771d6fdd1349955c2d0f500ccf34c2109507b (patch) | |
| tree | 1bb75c17f846a185c88bcd332e5890ebb2c41076 /tactics/rewrite.ml | |
| parent | e8a531dfa623e3badc3baddcf13f0a7975c37886 (diff) | |
Improving error message when applying rewrite to an expression which is not an equality.
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |