[api] Move `Constrexpr` to the `interp` module.

Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.

This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.

This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.

IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.

1 files changed, 0 insertions, 6 deletions

diff --git a/library/misctypes.ml b/library/misctypes.ml
index a3c887045..cfae07484 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -112,9 +112,3 @@ type multi =
   | UpTo of int
   | RepeatStar
   | RepeatPlus
-
-type ('a, 'b) gen_universe_decl = {
-  univdecl_instance : 'a; (* Declared universes *)
-  univdecl_extensible_instance : bool; (* Can new universes be added *)
-  univdecl_constraints : 'b; (* Declared constraints *)
-  univdecl_extensible_constraints : bool (* Can new constraints be added *) }