aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/constr_matching.ml1
-rw-r--r--pretyping/constrexpr.ml153
-rw-r--r--pretyping/detyping.ml1
-rw-r--r--pretyping/genredexpr.ml66
-rw-r--r--pretyping/glob_ops.ml1
-rw-r--r--pretyping/miscops.ml21
-rw-r--r--pretyping/miscops.mli6
-rw-r--r--pretyping/pretyping.ml1
-rw-r--r--pretyping/pretyping.mllib4
-rw-r--r--pretyping/redops.ml44
-rw-r--r--pretyping/redops.mli15
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/typeclasses.ml6
-rw-r--r--pretyping/typeclasses.mli16
-rw-r--r--pretyping/typeclasses_errors.ml4
-rw-r--r--pretyping/typeclasses_errors.mli4
-rw-r--r--pretyping/typing.ml1
-rw-r--r--pretyping/univdecls.ml52
-rw-r--r--pretyping/univdecls.mli21
20 files changed, 18 insertions, 402 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c9c2445a7..bf9e37aa7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -20,6 +20,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Environ
open EConstr
open Vars
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0ff6a330f..22da5315f 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -13,6 +13,7 @@ open Pp
open CErrors
open Util
open Names
+open Constr
open Globnames
open Termops
open Term
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/detyping.ml b/pretyping/detyping.ml
index fc398df9a..e6cfe1f76 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -14,6 +14,7 @@ open Pp
open CErrors
open Util
open Names
+open Constr
open Term
open EConstr
open Vars
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/glob_ops.ml b/pretyping/glob_ops.ml
index 5056c0457..63618c918 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -11,6 +11,7 @@
open Util
open CAst
open Names
+open Constr
open Nameops
open Globnames
open Misctypes
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.ml b/pretyping/pretyping.ml
index de72f9427..92f87ab95 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,6 +28,7 @@ open CErrors
open Util
open Names
open Evd
+open Constr
open Term
open Termops
open Environ
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/tacred.ml b/pretyping/tacred.ml
index 5a47acd22..40c4cfaa4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Libnames
open Globnames
open Termops
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 12a944d32..70588b6ad 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
let typeclasses_unique_solutions = ref false
let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
@@ -80,7 +80,7 @@ type typeclass = {
cl_props : Context.Rel.t;
(* The method implementaions as projections. *)
- cl_projs : (Name.t * (direction * hint_info_expr) option
+ cl_projs : (Name.t * (direction * hint_info) option
* Constant.t option) list;
cl_strict : bool;
@@ -92,7 +92,7 @@ type typeclasses = typeclass Refmap.t
type instance = {
is_class: GlobRef.t;
- is_info: hint_info_expr;
+ is_info: hint_info;
(* Sections where the instance should be redeclared,
None for discard, Some 0 for none. *)
is_global: int option;
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2a8e0b874..c78382c82 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
(** This module defines type-classes *)
type typeclass = {
@@ -44,7 +44,7 @@ type typeclass = {
Some may be undefinable due to sorting restrictions or simply undefined if
no name is provided. The [int option option] indicates subclasses whose hint has
the given priority. *)
- cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list;
+ cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list;
(** Whether we use matching or full unification during resolution *)
cl_strict : bool;
@@ -62,7 +62,7 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> hint_info_expr -> bool -> GlobRef.t -> instance
+val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit
@@ -129,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state
val add_instance_hint_hook :
(global_reference_or_constr -> GlobRef.t list ->
- bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
+ bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t
val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t
val add_instance_hint : global_reference_or_constr -> GlobRef.t list ->
- bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit
+ bool -> hint_info -> Decl_kinds.polymorphic -> unit
val remove_instance_hint : GlobRef.t -> unit
val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
-val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit
+val declare_instance : hint_info option -> bool -> GlobRef.t -> unit
(** Build the subinstances hints for a given typeclass object.
@@ -146,5 +146,5 @@ val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit
subinstances and add only the missing ones. *)
val build_subclasses : check:bool -> env -> evar_map -> GlobRef.t ->
- hint_info_expr ->
- (GlobRef.t list * hint_info_expr * constr) list
+ hint_info ->
+ (GlobRef.t list * hint_info * constr) list
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/typing.ml b/pretyping/typing.ml
index 68f9610d1..bffe36eea 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -14,6 +14,7 @@ open Pp
open CErrors
open Util
open Term
+open Constr
open Environ
open EConstr
open Vars
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 03:28:44 +0000