diff options
| author | SimonBoulier | 2019-06-03 17:17:35 +0200 |
|---|---|---|
| committer | SimonBoulier | 2019-08-16 11:43:51 +0200 |
| commit | 24701948804ecdc7c2518773fd66308913441195 (patch) | |
| tree | 3798eba8aa44c78ef22004b3eab8069fc2a317fe /test-suite | |
| parent | de02e40124e4938fd4796303b8f5686e542fcb1a (diff) | |
Universe Checking instead of Universes Checking
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/typing_flags.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index 31550b45a6..c15701e000 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -16,13 +16,13 @@ Set Guard Checking. Print Assumptions f. -Unset Universes Checking. +Unset Universe Checking. Definition T := Type. Fixpoint g (n : nat) : T := T. Print Typing Flags. -Set Universes Checking. +Set Universe Checking. Fail Definition g2 (n : nat) : T := T. |