Credit

clarus · clarus · commit 74f2c33cae7b · 2015-03-24T18:21:28.000+01:00
diff --git a/All.v b/All.v
@@ -1,3 +1,5 @@
+(** The following proof is due to a bug in `vm_compute` and was found by
+    Maxime Dénès and Pierre-Marie Pédrot. *)
 Inductive t :=
 | C_0 : nat -> t
 | C_1 : nat -> t

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,5 @@`
	`1`	+(** The following proof is due to a bug in `vm_compute` and was found by
	`2`	`+ Maxime Dénès and Pierre-Marie Pédrot. *)`
`1`	`3`	`Inductive t :=`
`2`	`4`	`\| C_0 : nat -> t`
`3`	`5`	`\| C_1 : nat -> t`