diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Fixpoint.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 81c9763ccd..ce3fddf249 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -96,10 +96,14 @@ Section visibility. Let Fixpoint by_proof (n:nat) : True. Proof. exact I. Defined. + + Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool. + Admitted. End visibility. Fail Check imm. Fail Check by_proof. +Check bla. Check bli. Module Import mod_local. Fixpoint imm_importable (n:nat) : True := I. |