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.ml | 21 ---------------------
 1 file changed, 21 deletions(-)

(limited to 'pretyping/miscops.ml')

diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 1b536bfda3..1697e54aba 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -10,7 +10,6 @@
 
 open Util
 open Misctypes
-open Genredexpr
 
 (** Mapping [cast_type] *)
 
@@ -42,26 +41,6 @@ let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
 | IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
 | _ -> false
 
-(** Mapping [red_expr_gen] *)
-
-let map_flags f flags =
-  { flags with rConst = List.map f flags.rConst }
-
-let map_occs f (occ,e) = (occ,f e)
-
-let map_red_expr_gen f g h = function
-  | Fold l -> Fold (List.map f l)
-  | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
-  | Simpl (flags,occs_o) ->
-     Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o)
-  | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
-  | Cbv flags -> Cbv (map_flags g flags)
-  | Lazy flags -> Lazy (map_flags g flags)
-  | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o)
-  | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
-  | Cbn flags -> Cbn (map_flags g flags)
-  | ExtraRedExpr _ | Red _ | Hnf as x -> x
-
 (** Mapping bindings *)
 
 let map_explicit_bindings f l =
-- 
cgit v1.2.3