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

1 files 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]