Skip to content
Snippets Groups Projects
Commit d0fdaa32 authored by Ralf Jung's avatar Ralf Jung
Browse files

warn users against importing the options file

parent 305121db
No related branches found
No related tags found
No related merge requests found
(** Coq configuration for Iris (not meant to leak to clients) *) (** Coq configuration for Iris (not meant to leak to clients).
If you are a user of Iris, note that importing this file means
you are implicitly opting-in to every new option we will add here
in the future. We are *not* guaranteeing any kind of stability here.
Instead our advice is for you to have your own options file; then
you can re-export the Iris file there but if we ever add an option
you disagree with you can easily overwrite it in one central location. *)
(* Everything here should be [Export Set], which means when this (* Everything here should be [Export Set], which means when this
file is *imported*, the option will only apply on the import site file is *imported*, the option will only apply on the import site
but not transitively. *) but not transitively. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment