Fixing #4859 (anomaly with Scheme called on inductive type with indices).

We raise a normal error instead of an anomaly.

1 files changed, 7 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4859.v b/test-suite/bugs/closed/4859.v
new file mode 100644
index 0000000000..7be0bedcfc
--- /dev/null
+++ b/test-suite/bugs/closed/4859.v
@@ -0,0 +1,7 @@
+(* Not supported but check at least that it does not raise an anomaly *)
+
+Inductive Fin{n : nat} : Set :=
+| F1{i : nat}{e : n = S i}
+| FS{i : nat}(f : @ Fin i){e : n = S i}.
+
+Fail Scheme Equality for Fin.