diff options
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. |