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/redops.ml | 44 --------------------------------------------
 1 file changed, 44 deletions(-)
 delete mode 100644 pretyping/redops.ml

(limited to 'pretyping/redops.ml')

diff --git a/pretyping/redops.ml b/pretyping/redops.ml
deleted file mode 100644
index 90c3bdfae6..0000000000
--- a/pretyping/redops.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Genredexpr
-
-let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
-
-let make_red_flag l =
-  let rec add_flag red = function
-    | [] -> red
-    | FBeta :: lf -> add_flag { red with rBeta = true } lf
-    | FMatch :: lf -> add_flag { red with rMatch = true } lf
-    | FFix :: lf -> add_flag { red with rFix = true } lf
-    | FCofix :: lf -> add_flag { red with rCofix = true } lf
-    | FZeta :: lf -> add_flag { red with rZeta = true } lf
-    | FConst l :: lf ->
-	if red.rDelta then
-	  CErrors.user_err Pp.(str
-	    "Cannot set both constants to unfold and constants not to unfold");
-        add_flag { red with rConst = union_consts red.rConst l } lf
-    | FDeltaBut l :: lf ->
-	if red.rConst <> [] && not red.rDelta then
-	  CErrors.user_err Pp.(str
-	    "Cannot set both constants to unfold and constants not to unfold");
-        add_flag
-          { red with rConst = union_consts red.rConst l; rDelta = true }
-          lf
-  in
-  add_flag
-    {rBeta = false; rMatch = false; rFix = false; rCofix = false;
-     rZeta = false; rDelta = false; rConst = []}
-    l
-
-
-let all_flags =
-  {rBeta = true; rMatch = true; rFix = true; rCofix = true;
-   rZeta = true; rDelta = true; rConst = []}
-- 
cgit v1.2.3