diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-12 14:14:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-12 15:10:30 +0100 |
| commit | 0c11bc39927c7756a0e3c3a6c445f20d0daaad7f (patch) | |
| tree | 39a53913a6ff2deb6f5597507780d9479ce62488 /test-suite | |
| parent | db002583b18c8742c0cd8e1a12305166b6b791ce (diff) | |
Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.
We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4412.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v new file mode 100644 index 000000000..4b2aae0c7 --- /dev/null +++ b/test-suite/bugs/closed/4412.v @@ -0,0 +1,4 @@ +Require Import Coq.Bool.Bool Coq.Setoids.Setoid. +Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True. + intros. + Fail rewrite Bool.andb_true_iff in H. |