From c7480636bce632adfa28d6bb0b423a086ade4318 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Aug 2014 11:33:08 +0200 Subject: Upgrading output tests. output/Arguments.v output/ArgumentsScope.v output/Arguments_renaming.v output/Cases.v output/Implicit.v output/PrintInfos.v output/TranspModType.v Main changes: monomorphic -> not universe polymorphic, Peano vs Nat --- test-suite/output/Arguments.out | 66 ++++++++++++++++---------------- test-suite/output/Arguments.v | 22 +++++------ test-suite/output/ArgumentsScope.out | 28 +++++++------- test-suite/output/Arguments_renaming.out | 14 +++---- test-suite/output/Cases.out | 12 +++--- test-suite/output/Implicit.out | 2 +- test-suite/output/PrintInfos.out | 32 ++++++++-------- test-suite/output/PrintInfos.v | 6 +-- test-suite/output/TranspModtype.out | 8 ++-- 9 files changed, 95 insertions(+), 95 deletions(-) (limited to 'test-suite') diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index e0e8211d5..dc421830f 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,48 +1,48 @@ -minus : nat -> nat -> nat +Nat.sub : nat -> nat -> nat -minus is monomorphic +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold minus avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +The reduction tactics unfold Nat.sub avoiding to expose match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat -minus is monomorphic +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold minus when applied to 1 argument +The reduction tactics unfold Nat.sub when applied to 1 argument avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat -minus is monomorphic +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold minus +The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and when applied to 1 argument avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat -minus is monomorphic +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold minus when the 1st and +The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat -minus is monomorphic +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold minus when the 1st and +The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor -minus is transparent -Expands to: Constant Coq.Init.Peano.minus +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub pf : forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 -pf is monomorphic +pf is not universe polymorphic Arguments D2, C2 are implicit Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] @@ -51,7 +51,7 @@ pf is transparent Expands to: Constant Top.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C -fcomp is monomorphic +fcomp is not universe polymorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] The reduction tactics unfold fcomp when applied to 6 arguments @@ -59,20 +59,20 @@ fcomp is transparent Expands to: Constant Top.fcomp volatile : nat -> nat -volatile is monomorphic +volatile is not universe polymorphic Argument scope is [nat_scope] The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Top.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat -f is monomorphic +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] f is transparent Expands to: Constant Top.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat -f is monomorphic +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor @@ -80,7 +80,7 @@ f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is monomorphic +f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and @@ -89,7 +89,7 @@ f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is monomorphic +f is not universe polymorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 5th, 6th and @@ -102,7 +102,7 @@ Expands to: Constant Top.f : Prop f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is monomorphic +f is not universe polymorphic The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 4d4ab54f1..05eeaac63 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -1,13 +1,13 @@ -Arguments minus n m : simpl nomatch. -About minus. -Arguments minus n / m : simpl nomatch. -About minus. -Arguments minus !n / m : simpl nomatch. -About minus. -Arguments minus !n !m /. -About minus. -Arguments minus !n !m. -About minus. +Arguments Nat.sub n m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub n / m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub !n / m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub !n !m /. +About Nat.sub. +Arguments Nat.sub !n !m. +About Nat.sub. Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := fun x => (f (fst x), g (snd x)). Delimit Scope foo_scope with F. @@ -44,7 +44,7 @@ Record r := { pi :> nat -> bool -> unit }. Notation "$" := 3 (only parsing) : foo_scope. Notation "$" := true (only parsing) : bar_scope. Delimit Scope bar_scope with B. -Arguments pi _ _%F _%B. +Arguments pi _ _%F _%B. Check (forall w : r, pi w $ $ = tt). Fail Check (forall w : r, w $ $ = tt). Axiom w : r. diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 358a96bc3..71d5fc78b 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,70 +1,70 @@ a : bool -> bool -a is monomorphic +a is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable a b : bool -> bool -b is monomorphic +b is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable b negb'' : bool -> bool -negb'' is monomorphic +negb'' is not universe polymorphic Argument scope is [bool_scope] negb'' is transparent Expands to: Constant Top.A.B.negb'' negb' : bool -> bool -negb' is monomorphic +negb' is not universe polymorphic Argument scope is [bool_scope] negb' is transparent Expands to: Constant Top.A.negb' negb : bool -> bool -negb is monomorphic +negb is not universe polymorphic Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool -a is monomorphic +a is not universe polymorphic Expands to: Variable a b : bool -> bool -b is monomorphic +b is not universe polymorphic Expands to: Variable b negb : bool -> bool -negb is monomorphic +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool -negb' is monomorphic +negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.A.negb' negb'' : bool -> bool -negb'' is monomorphic +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.A.B.negb'' a : bool -> bool -a is monomorphic +a is not universe polymorphic Expands to: Variable a negb : bool -> bool -negb is monomorphic +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool -negb' is monomorphic +negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.negb' negb'' : bool -> bool -negb'' is monomorphic +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.negb'' diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c440d5ba7..c99dfc018 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -20,7 +20,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 monomorphic +eq_refl is not universe polymorphic Arguments are renamed to B, y When applied to no arguments: Arguments B, y are implicit and maximally inserted @@ -36,7 +36,7 @@ For myEq: Argument scopes are [type_scope _ _] For myrefl: Argument scopes are [type_scope _ _] myrefl : forall (B : Type) (x : A), B -> myEq B x x -myrefl is monomorphic +myrefl is not universe polymorphic Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] @@ -49,13 +49,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is monomorphic +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat -myplus is monomorphic +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -74,7 +74,7 @@ For myEq: Argument scopes are [type_scope type_scope _ _] For myrefl: Argument scopes are [type_scope type_scope _ _] myrefl : forall (A B : Type) (x : A), B -> myEq A B x x -myrefl is monomorphic +myrefl is not universe polymorphic Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] @@ -89,13 +89,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is monomorphic +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat -myplus is monomorphic +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 152a722aa..c768f09ce 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -t_rect is monomorphic +t_rect is not universe polymorphic proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with @@ -18,7 +18,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -proj is monomorphic +proj is not universe polymorphic Argument scopes are [nat_scope nat_scope _ _ _] foo = fix foo (A : Type) (l : list A) {struct l} : option A := @@ -29,7 +29,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -foo is monomorphic +foo is not universe polymorphic Argument scopes are [type_scope list_scope] uncast = fun (A : Type) (x : I A) => match x with @@ -37,12 +37,12 @@ fun (A : Type) (x : I A) => match x with end : forall A : Type, I A -> A -uncast is monomorphic +uncast is not universe polymorphic Argument scopes are [type_scope _] foo' = if A 0 then true else false : bool -foo' is monomorphic +foo' is not universe polymorphic f = fun H : B => match H with @@ -54,4 +54,4 @@ match H with end : B -> True -f is monomorphic +f is not universe polymorphic diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index d1cd5e84f..0b0f501f9 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -d2 is monomorphic +d2 is not universe polymorphic Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 62889f802..2b010f067 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -25,7 +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 monomorphic +eq_refl is not universe polymorphic When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -38,27 +38,27 @@ 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 -plus is monomorphic +Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] -plus : nat -> nat -> nat +Nat.add : nat -> nat -> nat -plus is monomorphic +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 monomorphic +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 @@ -80,13 +80,13 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set -comparison is monomorphic +comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo -bar is monomorphic +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -94,14 +94,14 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is monomorphic +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 monomorphic +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -109,7 +109,7 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is monomorphic +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index deeb1f656..4edeeb232 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -6,9 +6,9 @@ Print eq_refl. About eq_refl. Print Implicit eq_refl. -Print plus. -About plus. -Print Implicit plus. +Print Nat.add. +About Nat.add. +Print Implicit Nat.add. About plus_n_O. diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index dbbd73dcd..67b65d4b8 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,15 +1,15 @@ TrM.A = M.A : Set -TrM.A is monomorphic +TrM.A is not universe polymorphic OpM.A = M.A : Set -OpM.A is monomorphic +OpM.A is not universe polymorphic TrM.B = M.B : Set -TrM.B is monomorphic +TrM.B is not universe polymorphic *** [ OpM.B : Set ] -OpM.B is monomorphic +OpM.B is not universe polymorphic -- cgit v1.2.3