diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-02-18 17:08:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-02-18 17:08:41 +0100 |
| commit | 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (patch) | |
| tree | 546fc22d794350fd0ba17750ba83ee394fbf0deb /tactics/rewrite.ml | |
| parent | cdbfad340dcd8cd3428853886964882b389776c6 (diff) | |
Fix bug #3938
Diffstat (limited to 'tactics/rewrite.ml')
| -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 c898ca401..ac8b4923e 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 |