diff options
| author | Hugo Herbelin | 2020-08-22 12:51:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 9cb28c30955db553f5e2b7abe7633dec97fa9dae (patch) | |
| tree | 49aea4f8b9d10405a2b76e6ccfdab7049cae7e74 | |
| parent | 1a91771fdc26bd0260ff26aceb91070217717d3b (diff) | |
Do not write "rename" for arguments in About, since these arguments are validated.
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 16 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 6 |
2 files changed, 9 insertions, 13 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index a5858fb056..8cc4383f49 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -23,11 +23,11 @@ Expands to: Constructor Coq.Init.Logic.eq_refl Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x Arguments myEq _%type_scope _ _ -Arguments myrefl {C}%type_scope x _ : rename +Arguments myrefl {C}%type_scope x _ myrefl : forall {C : Type} (x : A), C -> myEq C x x myrefl is not universe polymorphic -Arguments myrefl {C}%type_scope x _ : rename +Arguments myrefl {C}%type_scope x _ Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -37,11 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -52,11 +52,11 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x Arguments myEq (_ _)%type_scope _ _ -Arguments myrefl A%type_scope {C}%type_scope x _ : rename +Arguments myrefl A%type_scope {C}%type_scope x _ myrefl : forall (A : Type) {C : Type} (x : A), C -> myEq A C x x myrefl is not universe polymorphic -Arguments myrefl A%type_scope {C}%type_scope x _ : rename +Arguments myrefl A%type_scope {C}%type_scope x _ Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -68,11 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 722a27c432..037ad7db1d 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -320,11 +320,7 @@ let print_arguments ref = | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs in - let flags, renames = match Arguments_renaming.arguments_names ref with - | exception Not_found -> flags, [] - | [] -> flags, [] - | renames -> `Rename::flags, renames - in + let renames = try Arguments_renaming.arguments_names ref with Not_found -> [] in let scopes = Notation.find_arguments_scope ref in let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in |