diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-18 19:08:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-22 15:37:59 +0100 |
| commit | 75b7729d204c7bae280d859bb233750f7c4b543e (patch) | |
| tree | 18272b0bf95b42b2074532ce0c9d16cecd49beac /test-suite/output/Arguments_renaming.out | |
| parent | 0c5f0afffd37582787f79267d9841259095b7edc (diff) | |
Adding mention of shelved/given-up status in "Show Existentials".
Also changed the API of pr_subgoals now using labels.
Also removed a trailing space in printing existentials.
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 4df21ae35..e73312c67 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ notation scopes add ': clear scopes' [arguments-assert,vernacular] eq_refl : ?y = ?y where -?y : [ |- nat] +?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y |