From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/output/PrintInfos.out | 45 ++++++++++++++++++++++++++++------------
 1 file changed, 32 insertions(+), 13 deletions(-)

(limited to 'test-suite/output/PrintInfos.out')

diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 598bb728..0457c860 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,16 +1,17 @@
-existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P
+existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
+existT is template universe polymorphic
 Argument A is implicit
 Argument scopes are [type_scope _ _ _]
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
-    existT : forall x : A, P x -> sigT P
+    existT : forall x : A, P x -> {x : A & P x}
 
 For sigT: Argument A is implicit
 For existT: Argument A is implicit
 For sigT: Argument scopes are [type_scope type_scope]
 For existT: Argument scopes are [type_scope _ _ _]
-existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P
+existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
@@ -24,6 +25,7 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
+eq_refl is not universe polymorphic
 When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
@@ -36,28 +38,30 @@ 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) {struct n} : nat :=
+Nat.add = 
+fix add (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
-  | S p => S (plus p m)
+  | S p => S (add p m)
   end
      : nat -> nat -> nat
 
+Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-plus : nat -> nat -> nat
+Nat.add : nat -> nat -> nat
 
+Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-plus is transparent
-Expands to: Constant Coq.Init.Peano.plus
-plus : nat -> nat -> nat
+Nat.add is transparent
+Expands to: Constant Coq.Init.Nat.add
+Nat.add : nat -> nat -> nat
 
 plus_n_O : forall n : nat, n = n + 0
 
+plus_n_O is not universe polymorphic
 Argument scope is [nat_scope]
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
-Warning: Implicit Arguments is deprecated; use Arguments instead
 Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
 
@@ -76,12 +80,13 @@ For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
+comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
 Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
-Warning: Implicit Arguments is deprecated; use Arguments instead
 bar : foo
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -89,12 +94,14 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 bar : foo
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -102,6 +109,7 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -109,7 +117,6 @@ Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation existS2 := existT2
 Expands to: Notation Coq.Init.Specif.existS2
-Warning: Implicit Arguments is deprecated; use Arguments instead
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
@@ -128,3 +135,15 @@ For eq_refl, when applied to 1 argument:
   Argument A is implicit and maximally inserted
 For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
+n:nat
+
+Hypothesis of the goal context.
+h:(n <> newdef n)
+
+Hypothesis of the goal context.
+g:(nat -> nat)
+
+Constant (let in) of the goal context.
+h:(n <> newdef n)
+
+Hypothesis of the goal context.
-- 
cgit v1.2.3