coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Hello,

is there a way to turn on the "Impredicative Set" option in the interactive
mode (e.g. in Proof General)?

Vladimir.

[Coq-Club] Guard Condition, Christian Doczkal
- RE: [Coq-Club] Guard Condition, Georges Gonthier
  - Re: [Coq-Club] Guard Condition, Gert Smolka
    - RE: [Coq-Club] Guard Condition, Georges Gonthier
      - [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
        
        Re: [Coq-Club] Impredicative [ Set ], Gregory Malecha
        
        Message not available
        
        Message not available
        Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
        Re: [Coq-Club] Impredicative [ Set ], Gregory Malecha
        Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
        Re: [Coq-Club] Impredicative [ Set ], Pierre Courtieu
        
        [Coq-Club] messy behavior with universes, Vladimir Voevodsky
        [Coq-Club] Re: [coqdev] messy behavior with universes, Tom Prince
        [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky
        Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Carlos Simpson
        Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky