diff options
| author | Emilio Jesus Gallego Arias | 2019-10-30 15:25:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-30 15:25:19 +0100 |
| commit | 6b13decaa6ca82ce10566121fb38a12072ab2a0c (patch) | |
| tree | 2106cade4e1576fce5c7312f6eb518a4f65319cf /test-suite | |
| parent | dbcdc4e53758339d2a7eb96d19fbcffeb143154d (diff) | |
| parent | be4ebad76e7cb132fb890769fcc6a83a781c8522 (diff) | |
Merge PR #10973: Remove dead code in save_remaining_recthms
Ack-by: JasonGross
Reviewed-by: ejgallego
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. |