From 5d9d019b1978f1a3ebb8429fcf23d8da9bf52212 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 21 Feb 2011 18:05:41 +0000
Subject: Some fixes of the test-suite scripts

In particular, the Fail meta-command cannot for the moment catch a Syntax Error,
which is raised by Vernac.parse_sentence, before we even now that the line starts
by a Fail...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/NumbersSyntax.out |  4 ++--
 test-suite/output/PrintInfos.out    | 16 ++++++++++++----
 2 files changed, 14 insertions(+), 6 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out
index 57207b7be2..b2677b6ad1 100644
--- a/test-suite/output/NumbersSyntax.out
+++ b/test-suite/output/NumbersSyntax.out
@@ -13,9 +13,9 @@ I31
      = 710436486
      : int31
 2
-     : BigN.t_
+     : BigN.t'
 1000000000000000000
-     : BigN.t_
+     : BigN.t'
 2 + 2
      : bigN
 2 + 2
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 19d7e7c684..d60c8097c4 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -17,17 +17,26 @@ Argument A is implicit
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
-For eq_refl: Argument A is implicit
+For eq_refl, when applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument A is implicit
 For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
-Argument A is implicit
+When applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+When applied to 1 argument:
+  Argument A is implicit
 Argument scopes are [type_scope _]
 Expands to: Constructor Coq.Init.Logic.eq_refl
 eq_refl : forall (A : Type) (x : A), x = x
 
-Argument A is implicit
+When applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+When applied to 1 argument:
+  Argument A is implicit
 plus = 
 fix plus (n m : nat) : nat := match n with
                               | 0 => m
@@ -43,7 +52,6 @@ plus is transparent
 Expands to: Constant Coq.Init.Peano.plus
 plus : nat -> nat -> nat
 
-No implicit arguments
 plus_n_O : forall n : nat, n = n + 0
 
 Argument scope is [nat_scope]
-- 
cgit v1.2.3