Skip to content

Allow compiling against "dev" version of Coq

Ralf Jung requested to merge ralf/opam into master

This matches e.g. Iris allowing a "dev" version of std++: You can install a "dev" version to test stuff, but then you are responsible for making sure that these versions actually work together. We rely on that when testing things against Iris master every night, for which purpose we install Iris master as "dev" version.

Cc @jjourdan who, IIRC, argue for removing the dev version some time ago.

If we accept this here, I will send similar patches to (some of?) our other projects.

Edited by Ralf Jung

Merge request reports