diff options
| -rw-r--r-- | tactics/rewrite.ml | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3938.v | 7 |
2 files changed, 15 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 diff --git a/test-suite/bugs/closed/3938.v b/test-suite/bugs/closed/3938.v new file mode 100644 index 000000000..984431338 --- /dev/null +++ b/test-suite/bugs/closed/3938.v @@ -0,0 +1,7 @@ +Require Import Coq.Arith.PeanoNat. +Hint Extern 1 => admit : typeclass_instances. +Require Import Setoid. +Goal forall a b (f : nat -> Set) (R : nat -> nat -> Prop), + Equivalence R -> R a b -> f a = f b. + intros a b f H. + intros. Fail rewrite H1. |