# Issues with Require from stdpp
**URL:** https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892
**Category:** Using Rocq
**Created:** [January 4, 2026, 3:00pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892 "2026-01-04T15:00:32Z")
**Posts on this page:** 10
**Page:** 1
### Author:  [@emilia144](https://discourse.rocq-prover.org/u/emilia144)
#### Post date: [January 4, 2026, 3:00pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/1 "2026-01-04T15:00:32Z")
Hello,
I want to use some theorems from the `list` module of `stdpp`. I don’t want to `Import` it because it is a large library and it clutters the global namespace with notation and names that I want to use for other things (like `partition`). So, I tried doing the following:
```coq
From stdpp Require base list.
Check list.elem_of_cons. (* The reference list.elem_of_cons was not found in the current environment. *)
```
In previous versions of Rocq/Coq this worked fine, but after upgrading from 8.20.0 to 9.0.0 this no longer works. It seems that the `list` module re-exports `list_basics`, `list_monad` etc., which each internally define their own `list` module that exports its symbols (see [stdpp.list](https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.list.html#)), but this does not work well when using `Require` only…
Selective import `Import list_basics(elem_of_cons).` does work, but does not play well with notations like `Notation head := hd_error.`, and it would be rather tedious to do this for every symbol I want to refer to, and the documentation notes that I should not rely on the organization of these internal modules.
As a side note, it seems like the rocq-stdpp package that is listed on [Iris / stdpp · GitLab](https://gitlab.mpi-sws.org/iris/stdpp) does not exist in the repository that is listed there:
```auto
$ opam repo list
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
<><> Repository configuration for switch default ><><><><><><><><><><><><><><><>
1 rocq-released2 https://rocq-prover.github.io/opam/released/
2 rocq-released https://rocq-prover.org/opam/released
3 default https://opam.ocaml.org
$ opam install rocq-stdpp
[ERROR] No package named rocq-stdpp found.
```
I could not create an issue on the MPI-SWS gitlab because I cannot create an account there (“An error occurred while validating username“).
Thanks for any help!
---
### Author:  [@silene](https://discourse.rocq-prover.org/u/silene)
#### Post date: [January 5, 2026, 7:39am UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/2 "2026-01-05T07:39:57Z")
> [@emilia144](#):
>
> As a side note, it seems like the rocq-stdpp package that is listed on [Iris / stdpp · GitLab](https://gitlab.mpi-sws.org/iris/stdpp) does not exist in the repository that is listed there:
I guess they have chosen to rename the package but they have not yet released it under the new name. You can either use the latest released version, which is named `coq-stdpp`, or use their development version with a command akin to `opam pin add rocq-stdpp https://gitlab.mpi-sws.org/iris/stdpp.git`
---
### Author:  [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)
#### Post date: [January 6, 2026, 8:07am UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/3 "2026-01-06T08:07:53Z")
> [@emilia144](#):
>
> In previous versions of Rocq/Coq this worked fine, but after upgrading from 8.20.0 to 9.0.0 this no longer works. It seems that the `list` module re-exports `list_basics`, `list_monad` etc., which each internally define their own `list` module that exports its symbols (see [stdpp.list](https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.list.html#)), but this does not work well when using `Require` only…
Oh, so when a Rocq module `Eport`s other modules, it does not make those modules available under its own namespace?
That is very odd. IIRC the same _does_ happen when you use an explicit `Module` (we make use of that [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/base_logic/base_logic.v?ref_type=heads)), so somehow file modules and `Module` modules behave differently? Or is there something else going on?
> [@emilia144](#):
>
> As a side note, it seems like the rocq-stdpp package that is listed on [Iris / stdpp · GitLab](https://gitlab.mpi-sws.org/iris/stdpp) does not exist in the repository that is listed there:
As that readme explains, you need to add the Iris opam repo to get the latest development version.
> [@emilia144](#):
>
> I could not create an issue on the MPI-SWS gitlab because I cannot create an account there (“An error occurred while validating username“).
This is odd. Have you tried a different username? If yes, could you send me a DM with the username and email address you tried? I can forward that to the admins so they can have a look. Unfortunately spammers make it very hard to run a public gitlab instance, so our admins need to do very aggressive spam filtering.
---
### Author:  [@silene](https://discourse.rocq-prover.org/u/silene)
#### Post date: [January 6, 2026, 12:30pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/4 "2026-01-06T12:30:17Z")
> [@RalfJ](#):
>
> Oh, so when a Rocq module `Eport`s other modules, it does not make those modules available under its own namespace?
>
> That is very odd. IIRC the same _does_ happen when you use an explicit `Module` (we make use of that [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/base_logic/base_logic.v?ref_type=heads)), so somehow file modules and `Module` modules behave differently?
What do you mean? The commands `Import` and `Export` are purely about visibility. They never reroot any symbol under a new module, be it a file module or a `Module` module.
```coq
Module Foo.
Module M.
Definition bar := O.
End M.
End Foo.
Module Baz.
Export Foo.M.
End Baz.
Fail Check Baz.bar.
Fail Check Baz.M.bar.
Fail Check Baz.Foo.M.bar.
Succeed Check Foo.M.bar.
```
---
### Author:  [@emilia144](https://discourse.rocq-prover.org/u/emilia144)
#### Post date: [January 6, 2026, 1:48pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/5 "2026-01-06T13:48:25Z")
> [@silene](#):
>
> The commands `Import` and `Export` are purely about visibility. They never reroot any symbol under a new module, be it a file module or a `Module` module.
Okay I guess this answers my question why it is like this. It is just not what I would have expected coming from programming languages like C++/Rust where `using`/`use` do work like this.
Still I’d like to know if there is any way to do `Require` on all of these list sub-modules and be able to refer to all the symbols by `list.symbol_name`. (Or, in your example, do some variation of `Require Baz` and then use `Baz.bar`.) If I can’t do this it means I cannot really upgrade to the newer std++ version because I would need to change the style of my 22,000 line repo…
---
### Author:  [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)
#### Post date: [January 6, 2026, 1:56pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/6 "2026-01-06T13:56:33Z")
> [@silene](#):
>
> What do you mean? The commands `Import` and `Export` are purely about visibility. They never reroot any symbol under a new module, be it a file module or a `Module` module.
Ah, we must be doing something else different for the other module then.
It’s a shame that the Rocq module system seems to have no proper support for “facades”, where the internal module organization is hidden from the public API.
> [@emilia144](#):
>
> Still I’d like to know if there is any way to do `Require` on all of these list sub-modules and be able to refer to all the symbols by `list.symbol_name`. (Or, in your example, do some variation of `Require Baz` and then use `Baz.bar`.) If I can’t do this it means I cannot really upgrade to the newer std++ version because I would need to change the style of my 22,000 line repo…
I would suggest you file an std++ issue but we have to first resolve the problem with the gitlab account for that – see my comment in the previous post. Meanwhile, I have [created an issue](https://gitlab.mpi-sws.org/iris/stdpp/-/issues/250) for you.
All the symbols in `list_basics` etc are already wrapped in a `list` module, so it should be possible to refer to them as such. But clearly some further trickery is needed to make this actually work.
---
### Author:  [@emilia144](https://discourse.rocq-prover.org/u/emilia144)
#### Post date: [January 6, 2026, 1:57pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/7 "2026-01-06T13:57:25Z")
> [@RalfJ](#):
>
> As that readme explains, you need to add the Iris opam repo to get the latest development version.
Oh I assumed that there was already a stable version of rocq-stdpp but this is not true.
> [@RalfJ](#):
>
> This is odd. Have you tried a different username? If yes, could you send me a DM with the username and email address you tried? I can forward that to the admins so they can have a look. Unfortunately spammers make it very hard to run a public gitlab instance, so our admins need to do very aggressive spam filtering.
Thank you, I ended up logging in through github. On [Sign up · GitLab](https://gitlab.mpi-sws.org/users/sign_up) I have tried different usernames including ones that are just random characters but in the console I see a 401 response with error “You must be authenticated to access this path.” When I click “Sign up” anyway, it redirects me to the sign-in page, seemingly without actually having created the account.
> [@RalfJ](#):
>
> I would suggest you file an std++ issue
Okay I will look at the issue you made.
---
### Author:  [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)
#### Post date: [January 6, 2026, 1:59pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/8 "2026-01-06T13:59:43Z")
> [@emilia144](#):
>
> Thank you, I ended up logging in through github.
Yes, that is the only way AFAIK. I don’t know how you even found the other form, the website does not link to it at all. You can’t use a random URL on a server that’s not linked anywhere and then expect that to work (and then not even mention that you used such a hidden URL when you talk about things not working!).
---
### Author:  [@emilia144](https://discourse.rocq-prover.org/u/emilia144)
#### Post date: [January 6, 2026, 2:07pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/9 "2026-01-06T14:07:34Z")
I didn’t know it was a hidden URL and that it wasn’t linked from anywhere… it seems like bad UI that a user should infer that the publicly accessible [Sign in · GitLab](https://gitlab.mpi-sws.org/users/sign_in) page with the “username” and “password” fields also has no way to be used because you cannot create a username and password. But maybe that is just how gitlab works, I don’t know.
---
### Author:  [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)
#### Post date: [January 6, 2026, 2:26pm UTC](https://discourse.rocq-prover.org/t/issues-with-require-from-stdpp/2892/10 "2026-01-06T14:26:11Z")
> [@emilia144](#):
>
> I didn’t know it was a hidden URL and that it wasn’t linked from anywhere
I mean, you clearly entered the URL in the URL bar without clicking a link. 😂 That’s not a “supported” way of interacting with any website I am aware of.
I agree the UI isn’t great, but it is just how gitlab works when local registration is disabled (and it sadly had to be disabled due to an enormous amount of spam bots, and no good tools in gitlab to deal with them).