diff options
| author | Gaëtan Gilbert | 2020-07-20 10:46:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-20 10:46:17 +0200 |
| commit | d6aff7758936e4028614a1ac7e1dfbc5c7f82076 (patch) | |
| tree | c4439ad667aab9dd6418af1ab81c8b31f97670f6 /test-suite | |
| parent | e9061bb414dfebad5bdf2efe634030563f8a2381 (diff) | |
| parent | a89bde7b31393947c2c52e2dc75c61aa9cbf9e8e (diff) | |
Merge PR #12684: Do not print constructor and inductive types as terms when asked to be printed as themselves
Reviewed-by: SkySkimmer
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ba316ceb64..b8db52735d 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,7 +7,7 @@ bli : Type Axioms: bli : Type Axioms: -@seq relies on definitional UIP. +seq relies on definitional UIP. Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g |