From 2a69be9e8243fa67d5c7ef5f10e623b02a0a3e2f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 21 May 2018 19:21:26 +0200
Subject: [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.
---
 vernac/comFixpoint.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/comFixpoint.mli')

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 36c2993afe..a6992a30b2 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -49,7 +49,7 @@ val interp_recursive :
   structured_fixpoint_expr list -> decl_notation list ->
 
   (* env / signature / univs / evar_map *)
-  (Environ.env * EConstr.named_context * Univdecls.universe_decl * Evd.evar_map) *
+  (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
   (Id.t list * Constr.constr option list * Constr.types list) *
   (* ctx per mutual def / implicits / struct annotations *)
@@ -74,19 +74,19 @@ type recursive_preentry =
 val interp_fixpoint :
   cofix:bool ->
   structured_fixpoint_expr list -> decl_notation list ->
-  recursive_preentry * Univdecls.universe_decl * UState.t *
+  recursive_preentry * UState.universe_decl * UState.t *
   (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 (** [Not used so far] *)
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * Univdecls.universe_decl * UState.t *
+  recursive_preentry * UState.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic ->
-  recursive_preentry * Univdecls.universe_decl * UState.t *
+  recursive_preentry * UState.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
-- 
cgit v1.2.3