[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.

11 files changed, 0 insertions, 390 deletions

diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml
deleted file mode 100644
index 1443dfb51..000000000
--- a/pretyping/constrexpr.ml
+++ /dev/null
@@ -1,153 +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 Names
-open Libnames
-open Misctypes
-open Decl_kinds
-
-(** {6 Concrete syntax for terms } *)
-
-(** [constr_expr] is the abstract syntax tree produced by the parser *)
-
-type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl
-
-type ident_decl = lident * universe_decl_expr option
-type name_decl = lname * universe_decl_expr option
-
-type notation = string
-
-type explicitation =
-  | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
-  | ExplByName of Id.t
-
-type binder_kind =
-  | Default of binding_kind
-  | Generalized of binding_kind * binding_kind * bool
-      (** Inner binding, outer bindings, typeclass-specific flag
-	 for implicit generalization of superclasses *)
-
-type abstraction_kind = AbsLambda | AbsPi
-
-type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
-
-(** Representation of integer literals that appear in Coq scripts.
-    We now use raw strings of digits in base 10 (big-endian), and a separate
-    sign flag. Note that this representation is not unique, due to possible
-    multiple leading zeros, and -0 = +0 *)
-
-type sign = bool
-type raw_natural_number = string
-
-type prim_token =
-  | Numeral of raw_natural_number * sign
-  | String of string
-
-type instance_expr = Glob_term.glob_level list
-
-type cases_pattern_expr_r =
-  | CPatAlias of cases_pattern_expr * lname
-  | CPatCstr  of reference
-    * cases_pattern_expr list option * cases_pattern_expr list
-  (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
-  | CPatAtom of reference option
-  | CPatOr   of cases_pattern_expr list
-  | CPatNotation of notation * cases_pattern_notation_substitution
-    * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
-				  (notation n applied with substitution l1)
-				  applied to arguments l2 *)
-  | CPatPrim   of prim_token
-  | CPatRecord of (reference * cases_pattern_expr) list
-  | CPatDelimiters of string * cases_pattern_expr
-  | CPatCast   of cases_pattern_expr * constr_expr
-and cases_pattern_expr = cases_pattern_expr_r CAst.t
-
-and cases_pattern_notation_substitution =
-    cases_pattern_expr list *     (** for constr subterms *)
-    cases_pattern_expr list list  (** for recursive notations *)
-
-and constr_expr_r =
-  | CRef     of reference * instance_expr option
-  | CFix     of lident * fix_expr list
-  | CCoFix   of lident * cofix_expr list
-  | CProdN   of local_binder_expr list * constr_expr
-  | CLambdaN of local_binder_expr list * constr_expr
-  | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
-  | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
-  | CApp     of (proj_flag * constr_expr) *
-                (constr_expr * explicitation CAst.t option) list
-  | CRecord  of (reference * constr_expr) list
-
-  (* representation of the "let" and "match" constructs *)
-  | CCases of Constr.case_style   (* determines whether this value represents "let" or "match" construct *)
-            * constr_expr option  (* return-clause *)
-            * case_expr list
-            * branch_expr list    (* branches *)
-
-  | CLetTuple of lname list * (lname option * constr_expr option) *
-                 constr_expr * constr_expr
-  | CIf of constr_expr * (lname option * constr_expr option)
-         * constr_expr * constr_expr
-  | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
-  | CPatVar of patvar
-  | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
-  | CSort   of Glob_term.glob_sort
-  | CCast   of constr_expr * constr_expr cast_type
-  | CNotation of notation * constr_notation_substitution
-  | CGeneralization of binding_kind * abstraction_kind option * constr_expr
-  | CPrim of prim_token
-  | CDelimiters of string * constr_expr
-  | CProj of reference * constr_expr
-and constr_expr = constr_expr_r CAst.t
-
-and case_expr = constr_expr                 (* expression that is being matched *)
-              * lname option                (* as-clause *)
-	      * cases_pattern_expr option   (* in-clause *)
-
-and branch_expr =
-  (cases_pattern_expr list list * constr_expr) CAst.t
-
-and fix_expr =
-    lident * (lident option * recursion_order_expr) *
-      local_binder_expr list * constr_expr * constr_expr
-
-and cofix_expr =
-    lident * local_binder_expr list * constr_expr * constr_expr
-
-and recursion_order_expr =
-  | CStructRec
-  | CWfRec of constr_expr
-  | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
-
-(* Anonymous defs allowed ?? *)
-and local_binder_expr =
-  | CLocalAssum   of lname list * binder_kind * constr_expr
-  | CLocalDef     of lname * constr_expr * constr_expr option
-  | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
-
-and constr_notation_substitution =
-    constr_expr list *      (** for constr subterms *)
-    constr_expr list list * (** for recursive notations *)
-    cases_pattern_expr list *   (** for binders *)
-    local_binder_expr list list (** for binder lists (recursive notations) *)
-
-type constr_pattern_expr = constr_expr
-
-(** Concrete syntax for modules and module types *)
-
-type with_declaration_ast =
-  | CWith_Module of Id.t list CAst.t * qualid CAst.t
-  | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
-
-type module_ast_r =
-  | CMident of qualid
-  | CMapply of module_ast * module_ast
-  | CMwith  of module_ast * with_declaration_ast
-and module_ast = module_ast_r CAst.t
diff --git a/pretyping/genredexpr.ml b/pretyping/genredexpr.ml
deleted file mode 100644
index 80697461a..000000000
--- 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
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 1b536bfda..1697e54ab 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 =
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 1d4504541..6a84fb9eb 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
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c48decdb0..3d9b5d3cf 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -16,13 +16,10 @@ Evarsolve
 Recordops
 Evarconv
 Typing
-Constrexpr
-Genredexpr
 Miscops
 Glob_term
 Ltac_pretype
 Glob_ops
-Redops
 Pattern
 Patternops
 Constr_matching
@@ -37,4 +34,3 @@ Indrec
 Cases
 Pretyping
 Unification
-Univdecls
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
deleted file mode 100644
index 90c3bdfae..000000000
--- 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 = []}
diff --git a/pretyping/redops.mli b/pretyping/redops.mli
deleted file mode 100644
index 285931ecd..000000000
--- a/pretyping/redops.mli
+++ /dev/null
@@ -1,15 +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
-
-val make_red_flag : 'a red_atom list -> 'a glob_red_flag
-
-val all_flags : 'a glob_red_flag
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 89c5d7e7b..a1ac53c73 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -12,7 +12,6 @@
 open Names
 open EConstr
 open Environ
-open Constrexpr
 (*i*)
 
 type contexts = Parameters | Properties
@@ -20,7 +19,6 @@ type contexts = Parameters | Properties
 type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
-    | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
@@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err))
 let not_a_class env c = typeclass_error env (NotAClass c)
 
 let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
-
-let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 4aabc0aee..1003f2ae1 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -11,14 +11,12 @@
 open Names
 open EConstr
 open Environ
-open Constrexpr
 
 type contexts = Parameters | Properties
 
 type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
-  | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
@@ -26,5 +24,3 @@ val not_a_class : env -> constr -> 'a
 
 val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
 
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a
-
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
deleted file mode 100644
index 8864be576..000000000
--- a/pretyping/univdecls.ml
+++ /dev/null
@@ -1,52 +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 CErrors
-
-(** Local universes and constraints declarations *)
-type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-let default_univ_decl =
-  let open Misctypes in
-  { univdecl_instance = [];
-    univdecl_extensible_instance = true;
-    univdecl_constraints = Univ.Constraint.empty;
-    univdecl_extensible_constraints = true }
-
-let interp_univ_constraints env evd cstrs =
-  let interp (evd,cstrs) (u, d, u') =
-    let ul = Pretyping.interp_known_glob_level evd u in
-    let u'l = Pretyping.interp_known_glob_level evd u' in
-    let cstr = (ul,d,u'l) in
-    let cstrs' = Univ.Constraint.add cstr cstrs in
-    try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
-        evd, cstrs'
-    with Univ.UniverseInconsistency e ->
-      user_err ~hdr:"interp_constraint"
-        (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
-  in
-  List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-
-let interp_univ_decl env decl =
-  let open Misctypes in
-  let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
-  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = pl;
-    univdecl_extensible_instance = decl.univdecl_extensible_instance;
-    univdecl_constraints = cstrs;
-    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
-  in evd, decl
-
-let interp_univ_decl_opt env l =
-  match l with
-  | None -> Evd.from_env env, default_univ_decl
-  | Some decl -> interp_univ_decl env decl
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
deleted file mode 100644
index 305d045b1..000000000
--- a/pretyping/univdecls.mli
+++ /dev/null
@@ -1,21 +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)         *)
-(************************************************************************)
-
-(** Local universe and constraint declarations. *)
-type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-val default_univ_decl : universe_decl
-
-val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr ->
-                       Evd.evar_map * universe_decl
-
-val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option ->
-                       Evd.evar_map * universe_decl