From 771ec30a33cd528d40cfe7fa63f40a42e3042284 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 9 Feb 2020 11:40:52 +0100
Subject: Fix #11553: magicaly_constant_of_fixbody checks existence of made up
 constant

---
 test-suite/bugs/closed/bug_11553.v | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11553.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_11553.v b/test-suite/bugs/closed/bug_11553.v
new file mode 100644
index 0000000000..a4a4353cd6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11553.v
@@ -0,0 +1,34 @@
+Definition var := nat.
+Module Import A.
+Class Rename (term : Type) := rename : (var -> var) -> term -> term.
+End A.
+
+Inductive tm : Type :=
+  (* | tv : vl_ -> tm *)
+ with vl_ : Type :=
+  | var_vl : var -> vl_.
+
+Definition vl := vl_.
+
+Fixpoint tm_rename (sb : var -> var) (t : tm) : tm :=
+  let b := vl_rename : Rename vl in
+  match t with
+  end
+with
+vl_rename (sb : var -> var) v : vl :=
+  let a := tm_rename : Rename tm in
+  let b := vl_rename : Rename vl in
+  match v with
+  | var_vl x => var_vl (sb x)
+  end.
+
+Instance rename_vl : Rename vl := vl_rename.
+
+Lemma foo ξ x: rename_vl ξ (var_vl x) = var_vl x.
+(* Succeeds *)
+cbn. Abort.
+
+Lemma foo ξ x: rename ξ (var_vl x) = var_vl x.
+(* Fails *)
+cbn.
+Abort.
-- 
cgit v1.2.3