From f519a1f10531e2513014fa4bbee9431aa4546faa Mon Sep 17 00:00:00 2001
From: pboutill
Date: Tue, 31 Jan 2012 16:17:50 +0000
Subject: Fix consequence of pp bugfix in testsuite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14954 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/PrintInfos.out | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 40c786abf5..598bb72810 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -37,10 +37,11 @@ When applied to no arguments:
 When applied to 1 argument:
   Argument A is implicit
 plus = 
-fix plus (n m : nat) : nat := match n with
-                              | 0 => m
-                              | S p => S (plus p m)
-                              end
+fix plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (plus p m)
+  end
      : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-- 
cgit v1.2.3