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

(limited to 'pretyping/genredexpr.ml')

diff --git a/pretyping/genredexpr.ml b/pretyping/genredexpr.ml
deleted file mode 100644
index 80697461a6..0000000000
--- a/pretyping/genredexpr.ml
+++ /dev/null
@@ -1,66 +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)         *)
-(************************************************************************)
-
-(** Reduction expressions *)
-
-(** The parsing produces initially a list of [red_atom] *)
-
-type 'a red_atom =
-  | FBeta
-  | FMatch
-  | FFix
-  | FCofix
-  | FZeta
-  | FConst of 'a list
-  | FDeltaBut of 'a list
-
-(** This list of atoms is immediately converted to a [glob_red_flag] *)
-
-type 'a glob_red_flag = {
-  rBeta : bool;
-  rMatch : bool;
-  rFix : bool;
-  rCofix : bool;
-  rZeta : bool;
-  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
-  rConst : 'a list
-}
-
-(** Generic kinds of reductions *)
-
-type ('a,'b,'c) red_expr_gen =
-  | Red of bool
-  | Hnf
-  | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Cbn of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
-  | Unfold of 'b Locus.with_occurrences list
-  | Fold of 'a list
-  | Pattern of 'a Locus.with_occurrences list
-  | ExtraRedExpr of string
-  | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
-  | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
-
-type ('a,'b,'c) may_eval =
-  | ConstrTerm of 'a
-  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of Misctypes.lident * 'a
-  | ConstrTypeOf of 'a
-
-open Libnames
-open Constrexpr
-open Misctypes
-
-type r_trm = constr_expr
-type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
-
-type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
-- 
cgit v1.2.3