diff options
| -rw-r--r-- | parsing/prettyp.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/ArgumentsScope.out | 10 | ||||
| -rw-r--r-- | test-suite/output/Implicit.v | 2 | ||||
| -rw-r--r-- | test-suite/output/PrintInfos.out | 36 | ||||
| -rw-r--r-- | test-suite/output/PrintInfos.v | 10 |
5 files changed, 50 insertions, 10 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 3151fa6d07..e30979bf9b 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -120,7 +120,7 @@ let print_impargs_list prefix l = else [str "No implicit arguments"]))])]) l) let print_renames_list prefix l = - if l = [] then [prefix] else + if l = [] then [] else [add_colon prefix ++ str "Arguments are renamed to " ++ hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))] diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index c95f89c9f0..756e8ede9a 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -21,6 +21,11 @@ negb : bool -> bool Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead a : bool -> bool Expands to: Variable a @@ -54,8 +59,3 @@ negb'' : bool -> bool negb'' is transparent Expands to: Constant Top.negb'' -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index d50c98765f..7c9b89f9d2 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -36,7 +36,7 @@ Check map id (1::nil). Definition id' (A:Type) (x:A) := x. -Implicit Arguments id' [[A]]. +Arguments id' {A} x. Check map id' (1::nil). diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index a2e6a1cfbb..40c786abf5 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -56,6 +56,15 @@ plus_n_O : forall n : nat, n = n + 0 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 + +For le_S: Argument m is implicit +For le_S: Argument n is implicit and maximally inserted +For le: Argument scopes are [nat_scope nat_scope] +For le_n: Argument scope is [nat_scope] +For le_S: Argument scopes are [nat_scope nat_scope _] Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m @@ -69,6 +78,20 @@ comparison : Set 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 + +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted +Expands to: Constant Top.bar +*** [ bar : foo ] + +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted bar : foo Expanded type for implicit arguments @@ -85,6 +108,16 @@ 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 +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 and maximally inserted +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted @@ -94,6 +127,3 @@ 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 _] -Warning: Implicit Arguments is deprecated; use Arguments instead -Warning: Implicit Arguments is deprecated; use Arguments instead -Warning: Implicit Arguments is deprecated; use Arguments instead diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index 6a89f88098..deeb1f656b 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -15,6 +15,9 @@ About plus_n_O. Implicit Arguments le_S [[n] m]. Print le_S. +Arguments le_S {n} [m] _. (* Test new syntax *) +Print le_S. + About comparison. Print comparison. @@ -24,8 +27,15 @@ Implicit Arguments bar [x]. About bar. Print bar. +Arguments bar [x]. (* Test new syntax *) +About bar. +Print bar. + About Peano. (* Module *) About existS2. (* Notation *) Implicit Arguments eq_refl [[A] [x]] [[A]]. Print eq_refl. + +Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *) +Print eq_refl. |