summaryrefslogtreecommitdiff
path: root/test-suite/output/Fixpoint.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Fixpoint.v')
-rw-r--r--test-suite/output/Fixpoint.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 2b13c204..af5f05f6 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -1,7 +1,7 @@
Require Import List.
Check
- (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} :
+ (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} :
list B := match l with
| nil => nil
| a :: l => f a :: F _ _ f l