diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 | ||||
| -rw-r--r-- | pretyping/constrexpr.ml | 6 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 1 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 19 | ||||
| -rw-r--r-- | pretyping/miscops.ml | 2 | ||||
| -rw-r--r-- | pretyping/miscops.mli | 2 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 2 | ||||
| -rw-r--r-- | pretyping/vernacexpr.ml | 2 |
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 |