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.
---
 pretyping/miscops.mli | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'pretyping/miscops.mli')

diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 1d45045414..6a84fb9eb2 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Misctypes
-open Genredexpr
 
 (** Mapping [cast_type] *)
 
@@ -25,11 +24,6 @@ val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 val intro_pattern_naming_eq :
   intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
 
-(** Mapping [red_expr_gen] *)
-
-val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
-  ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
-
 (** Mapping bindings *)
 
 val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
-- 
cgit v1.2.3