diff options
| author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2022-12-22 16:20:15 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-12-22 16:20:15 +0100 |
| commit | fc79b13a30f124e9ac2d658773c395e0a74e2d1e (patch) | |
| tree | f81eb0494f192d3abe40c7ce50a4bf77c9596766 /lib/Iteration.v | |
| parent | 8d21a7fa245637b684ddb4c12f4bfa6295569fb6 (diff) | |
| download | compcert-fc79b13a30f124e9ac2d658773c395e0a74e2d1e.tar.gz compcert-fc79b13a30f124e9ac2d658773c395e0a74e2d1e.zip | |
Use `exfalso` instead of `elimtype False` (#470)
Adapt w.r.t. coq/coq#16904.
Diffstat (limited to 'lib/Iteration.v')
| -rw-r--r-- | lib/Iteration.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Iteration.v b/lib/Iteration.v index 66bb3970..34471826 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -240,7 +240,7 @@ Lemma iter_monot: Proof. induction p; intros. simpl. red; intros; red; auto. - destruct q. elimtype False; lia. + destruct q. exfalso; lia. simpl. apply F_iter_monot. apply IHp. lia. Qed. |