diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c898ca401d..ac8b4923e5 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1444,7 +1444,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let newt = Evarutil.nf_evar evars' res.rew_to in let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) - Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars' + Evar.Set.fold + (fun ev acc -> + if not (Evd.is_defined acc ev) then + errorlabstrm "rewrite" + (str "Unsolved constraint remaining: " ++ spc () ++ + Evd.pr_evar_info (Evd.find acc ev)) + else Evd.remove acc ev) + cstrs evars' in let res = match res.rew_prf with | RewCast c -> None |