Emilio Jesús Gallego Arias

@herbelin based on your examples I'm not sure the PR is doing what you want? (Do examples compile at all?) I think you've modified the `Proof term` command

How does this compare to the existing `lock/unlock` mechanism?

@gares couldn't at least disable `deprecated-arguments-scope` and `deprecated-implicit-arguments` for now? The build log of math-comp is truly unreadable...

The warning situation has gotten out of hand; I'd suggest to silence the warnings, but filing the corresponding Coq issues first; it will take a while for Coq to address...

Hi folks, actually OCaml is not using the beta-repository anymore, instead they use this: ``` flags avoid-version depends "ocaml-beta" {opam-version < "2.1.0"} ``` I have also been told that the...

> So I believe the proposal here tries to solve a problem that very few people have, with high risk of introducing Coq version opam upgrade chaos. That's a problem...

> According to our discussion in https://github.com/coq/opam-coq-archive/pull/2439, @ejgallego seemingly wants (contrarily to OCaml approach) to have everything to do with RCs live in the released repo, so that regular users...

Sorry folks, I've moved the topic to Coq's Call next week, I can't make it today. I will answer to Enrico's question ASAP.

> So which is your conclusion @ejgallego ? what are you proposing on the end? A single repo with avoid-version or what? Thanks @gares for asking the question as indeed...

Hi @brando90 , I have no idea, I would guess at the current stage, pyCoq would be used to generate the datasets, and interact with Coq, but I am not...