diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:41:37 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:41:37 +0200 |
commit | d5de86d0606e1c3dc88c48bf3ec2e820b5485d8f (patch) | |
tree | 78d2bc44cd6778fca1c4f2c56cb668732dfeca8f /test-suite/success | |
parent | 3d10815dd3929f718fc4ede5d5a2a1fe5ccdc351 (diff) | |
parent | 92526ebd960d2a878b6a1066acc55f0754c4c824 (diff) |
Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Fixpoint.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 5fc703cf0..efb32ef6f 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -91,3 +91,33 @@ apply Cons2. exact b. apply (ex1 (S n) (negb b)). Defined. + +Section visibility. + + Let Fixpoint imm (n:nat) : True := I. + + Let Fixpoint by_proof (n:nat) : True. + Proof. exact I. Defined. +End visibility. + +Fail Check imm. +Fail Check by_proof. + +Module Import mod_local. + Fixpoint imm_importable (n:nat) : True := I. + + Local Fixpoint imm_local (n:nat) : True := I. + + Fixpoint by_proof_importable (n:nat) : True. + Proof. exact I. Defined. + + Local Fixpoint by_proof_local (n:nat) : True. + Proof. exact I. Defined. +End mod_local. + +Check imm_importable. +Fail Check imm_local. +Check mod_local.imm_local. +Check by_proof_importable. +Fail Check by_proof_local. +Check mod_local.by_proof_local. |