diff options
| author | Emilio Jesus Gallego Arias | 2018-04-24 03:26:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-08 01:13:04 +0200 |
| commit | a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f (patch) | |
| tree | 911c09c586a6d90a6d1e304e86260767a7b0bdbb /pretyping/constrexpr.ml | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
[api] Move universe syntax to `Glob_term`
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
Diffstat (limited to 'pretyping/constrexpr.ml')
| -rw-r--r-- | pretyping/constrexpr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml index fda31756a9..1443dfb513 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 |