diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 65f29498c..fb9ca2507 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1326,8 +1326,7 @@ let cl_rewrite_clause_newtac ?abs strat clause = | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (str"Unable to satisfy the rewriting constraints." ++ fnl () ++ Himsg.explain_typeclass_error env e))) - in - Proofview.tclGOALBINDU info (fun i -> treat i) + in Proofview.Notations.(>>-) (Proofview.Goal.lift info) (fun i -> treat i) let newtactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () @@ -1766,9 +1765,9 @@ let not_declared env ty rel = str ty ++ str" relation. Maybe you need to require the Setoid library") let setoid_proof ty fn fallback = - Goal.env >>- fun env -> - Goal.defs >>- fun sigma -> - Goal.concl >>- fun concl -> + Proofview.tclEVARMAP >= fun sigma -> + Proofview.Goal.env >>- fun env -> + Proofview.Goal.concl >>- fun concl -> Proofview.tclORELSE begin try |