diff options
Diffstat (limited to 'ltac/rewrite.ml')
| -rw-r--r-- | ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index b559864bd..8e74249de 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1502,7 +1502,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul Evar.Set.fold (fun ev acc -> if not (Evd.is_defined acc ev) then - errorlabstrm "rewrite" + user_err ~hdr:"rewrite" (str "Unsolved constraint remaining: " ++ spc () ++ Evd.pr_evar_info (Evd.find acc ev)) else Evd.remove acc ev) |