[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.

4 files changed, 8 insertions, 15 deletions

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 805635dfa..7b7973224 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -24,7 +24,7 @@ open Decl_kinds
     proof of mutually dependent theorems) *)
 
 val start_proof :
-  Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+  Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d5cb5b09f..3abdd129e 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -97,7 +97,7 @@ type pstate = {
   proof : Proof.t;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
-  universe_decl: Univdecls.universe_decl;
+  universe_decl: UState.universe_decl;
 }
 
 type t = pstate list
@@ -238,13 +238,6 @@ let activate_proof_mode mode =
 let disactivate_current_proof_mode () =
   CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
-let default_universe_decl =
-  let open Misctypes in
-  { univdecl_instance = [];
-    univdecl_extensible_instance = true;
-    univdecl_constraints = Univ.Constraint.empty;
-    univdecl_extensible_constraints = true }
-
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
@@ -253,7 +246,7 @@ let default_universe_decl =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
+let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -265,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
     universe_decl = pl } in
   push initial_state pstates
 
-let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
+let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index de4cec488..0141cacb9 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -71,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
+  Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
+  Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
@@ -130,7 +130,7 @@ val set_used_variables :
 val get_used_variables : unit -> Context.Named.t option
 
 (** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : unit -> Univdecls.universe_decl
+val get_universe_decl : unit -> UState.universe_decl
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index f9e7bbfac..03ebc3275 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -263,7 +263,7 @@ let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
 
 let subst_red_expr subs =
-  Miscops.map_red_expr_gen
+  Redops.map_red_expr_gen
     (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
     (Patternops.subst_pattern subs)