diff options
| author | Gaëtan Gilbert | 2019-10-26 10:25:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-26 15:07:15 +0200 |
| commit | be4ebad76e7cb132fb890769fcc6a83a781c8522 (patch) | |
| tree | 34927152331a9e96b514a0424370917582b29d1e /test-suite | |
| parent | f7659e6c5d197ddeff8509a4aab40316534b3a12 (diff) | |
Remove dead code in save_remaining_recthms
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. |