From c3aa4c065fac0e37d67ca001aec47b1c2138e648 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 14 Dec 2015 20:29:45 +0100 Subject: extraction_impl.v: fix a typo --- test-suite/success/extraction_impl.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/success') diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v index a72715f29..dfdeff82f 100644 --- a/test-suite/success/extraction_impl.v +++ b/test-suite/success/extraction_impl.v @@ -64,7 +64,7 @@ Fixpoint enat_nat' n (e:enat n) : nat := end. Extraction Implicit enat_nat' [n]. -Recursive Extraction enat_nat. +Recursive Extraction enat_nat'. (** Bug #4228 *) -- cgit v1.2.3