diff options
Diffstat (limited to 'test-suite/bugs/closed/38.v')
| -rw-r--r-- | test-suite/bugs/closed/38.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/38.v b/test-suite/bugs/closed/38.v index 4fc8d7c97..6b6e83779 100644 --- a/test-suite/bugs/closed/38.v +++ b/test-suite/bugs/closed/38.v @@ -14,7 +14,7 @@ Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m. Definition same_refl (x:liste) : (same x x). unfold same; split; intros; trivial. -Save. +Qed. Goal forall (x:liste), (same x x). intro. |