diff options
| author | Emilio Jesus Gallego Arias | 2020-11-18 23:25:17 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-26 21:21:55 +0100 |
| commit | 50af46a596af607493ce46da782389e8a82e8354 (patch) | |
| tree | 39f3b35a0a14148467819ed437ca36da8a8c2d2b /test-suite | |
| parent | 2ac3d11f6f1332250e918ef628eca3b788b3550a (diff) | |
[attributes] [doc] Documentation review by Théo.
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/typing_flags.v | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index a5fe676cc1..4a20f3379b 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -26,17 +26,11 @@ Print Assumptions att_T. Print Assumptions att_Cor. (* Interactive + atts *) - -(* Coq's handling of environments in tactic mode is too broken for - this to work yet, the pretyper doesn't get the right flags *) - #[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. #[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. #[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. -(* Note: this works a bit by chance, the attribute only affects the - kernel call in Defined. Would the tactics perform a check we would - fail. *) +(* Note: be aware of tactics invoking [Global.env()] if this test fails. *) #[typing(guarded=no)] Fixpoint i_att_f' (n : nat) : nat. Proof. exact (i_att_f' n). Defined. |