aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/constr_matching.ml2
-rw-r--r--pretyping/constrexpr.ml6
-rw-r--r--pretyping/detyping.mli1
-rw-r--r--pretyping/glob_term.ml19
-rw-r--r--pretyping/miscops.ml2
-rw-r--r--pretyping/miscops.mli2
-rw-r--r--pretyping/pattern.ml2
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/vernacexpr.ml2
10 files changed, 30 insertions, 12 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index b4e1a1b10..0ff6a330f 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -20,7 +20,6 @@ open EConstr
open Vars
open Pattern
open Patternops
-open Misctypes
open Context.Rel.Declaration
open Ltac_pretype
(*i*)
@@ -277,6 +276,7 @@ let matches_core env sigma allow_bound_rels
| PSort ps, Sort s ->
+ let open Glob_term in
begin match ps, ESorts.kind sigma s with
| GProp, Prop Null -> subst
| GSet, Prop Pos -> subst
diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml
index fda31756a..1443dfb51 100644
--- a/pretyping/constrexpr.ml
+++ b/pretyping/constrexpr.ml
@@ -17,7 +17,7 @@ open Decl_kinds
(** [constr_expr] is the abstract syntax tree produced by the parser *)
-type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+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
@@ -50,7 +50,7 @@ type prim_token =
| Numeral of raw_natural_number * sign
| String of string
-type instance_expr = Misctypes.glob_level list
+type instance_expr = Glob_term.glob_level list
type cases_pattern_expr_r =
| CPatAlias of cases_pattern_expr * lname
@@ -98,7 +98,7 @@ and constr_expr_r =
| 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_sort
+ | 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
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 817b8ba6e..5310455fe 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -14,7 +14,6 @@ open EConstr
open Glob_term
open Termops
open Mod_subst
-open Misctypes
open Evd
open Ltac_pretype
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 3c3f75a68..6ecb479e6 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -22,6 +22,25 @@ open Misctypes
type existential_name = Id.t
+(** Sorts *)
+
+type 'a glob_sort_gen =
+ | GProp (** representation of [Prop] literal *)
+ | GSet (** representation of [Set] literal *)
+ | GType of 'a (** representation of [Type] literal *)
+
+type 'a universe_kind =
+ | UAnonymous
+ | UUnknown
+ | UNamed of 'a
+
+type level_info = Libnames.reference universe_kind
+type glob_level = level_info glob_sort_gen
+type glob_constraint = glob_level * Univ.constraint_type * glob_level
+
+type sort_info = (Libnames.reference * int) option list
+type glob_sort = sort_info glob_sort_gen
+
(** The kind of patterns that occurs in "match ... with ... end"
locs here refers to the ident's location, not whole pat *)
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 0f0af5409..1b536bfda 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -29,7 +29,7 @@ let smartmap_cast_type f c =
(** Equalities on [glob_sort] *)
-let glob_sort_eq g1 g2 = match g1, g2 with
+let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
| GProp, GProp -> true
| GSet, GSet -> true
| GType l1, GType l2 ->
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index abe817fe5..1d4504541 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -18,7 +18,7 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
(** Equalities on [glob_sort] *)
-val glob_sort_eq : glob_sort -> glob_sort -> bool
+val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
(** Equalities on [intro_pattern_naming] *)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 7dd0954bc..996a2dc36 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -30,7 +30,7 @@ type constr_pattern =
| PLambda of Name.t * constr_pattern * constr_pattern
| PProd of Name.t * constr_pattern * constr_pattern
| PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
- | PSort of glob_sort
+ | PSort of Glob_term.glob_sort
| PMeta of patvar option
| PIf of constr_pattern * constr_pattern * constr_pattern
| PCase of case_info_pattern * constr_pattern * constr_pattern *
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 35cc5702a..616ccf0cf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -245,7 +245,7 @@ let interp_known_level_info ?loc evd = function
with Not_found ->
user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
-let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
+let interp_level_info ?loc evd : level_info -> _ = function
| UUnknown -> new_univ_level_variable ?loc univ_rigid evd
| UAnonymous -> new_univ_level_variable ?loc univ_flexible evd
| UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s
@@ -499,7 +499,7 @@ let interp_known_glob_level ?loc evd = function
| GSet -> Univ.Level.set
| GType s -> interp_known_level_info ?loc evd s
-let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function
+let interp_glob_level ?loc evd : glob_level -> _ = function
| GProp -> evd, Univ.Level.prop
| GSet -> evd, Univ.Level.set
| GType s -> interp_level_info ?loc evd s
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 415c4e172..73f5b77e0 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ open Ltac_pretype
open Evardefine
val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
- Misctypes.glob_level -> Univ.Level.t
+ glob_level -> Univ.Level.t
(** An auxiliary function for searching for fixpoint guard indexes *)
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 3a49d6cf8..e15c3ad04 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -338,7 +338,7 @@ type nonrec vernac_expr =
| VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
| VernacUniverse of lident list
- | VernacConstraint of glob_constraint list
+ | VernacConstraint of Glob_term.glob_constraint list
(* Gallina extensions *)
| VernacBeginSection of lident