From 3910e8dca2154d15c422a8e5ceb16f93c5faf889 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 31 Oct 2019 13:17:15 +0100
Subject: Fix #8459: anomaly not enough abstractions in fix body

We reach the anomaly because we call check_fix on a surrounding
fixpoint from the pretyper, and the inner fix hasn't been checked.

Using whd_all isn't useful in the specific reported case but a case
where it's necessary can probably be crafted.

See also #11013
---
 test-suite/bugs/closed/bug_8459.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_8459.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_8459.v b/test-suite/bugs/closed/bug_8459.v
new file mode 100644
index 0000000000..62c49e9ea7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8459.v
@@ -0,0 +1,24 @@
+Require Import Coq.Vectors.Vector.
+
+Axiom exfalso : False.
+
+Fixpoint all_then_someV (n:nat) (l:Vector.t bool n) {struct l}:
+(Vector.fold_left orb false l) = false ->
+(forall p, (Vector.nth l p  ) = false).
+Proof.
+intros.
+destruct l.
+inversion p.
+revert h l H.
+set (P := fun n p => forall (h : bool) (l : t bool n),
+fold_left orb false (cons bool h n l) = false -> @eq bool (@nth bool (S n) (cons bool h n l) p) false).
+revert n p.
+fix loop 1.
+unshelve eapply (@Fin.rectS P).
++ elim exfalso.
++ unfold P.
+  intros.
+  eapply all_then_someV.
+  exact H0.
+Fail Defined.
+Abort.
-- 
cgit v1.2.3