Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence of made up constant

Reviewed-by: ppedrot

1 files changed, 34 insertions, 0 deletions

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.