diff options
| author | Gaëtan Gilbert | 2020-11-18 13:48:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-25 12:00:23 +0100 |
| commit | 2b80095f5dbfb996643309bfae6f45f62e2ecdb1 (patch) | |
| tree | da5f575b9568686099179b9988fc63fe65024819 /vernac | |
| parent | 075811dc6424d9c7663e7913b7d7d7735e9c2dac (diff) | |
Reserve "sort_expr" for uninterned universes
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacexpr.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index defb0691c0..89c09bb169 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -129,8 +129,6 @@ type option_setting = (** Identifier and optional list of bound universes and constraints. *) -type sort_expr = Sorts.family - type definition_expr = | ProveBody of local_binder_expr list * constr_expr | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr @@ -210,8 +208,8 @@ type proof_end = | Proved of opacity_flag * lident option type scheme = - | InductionScheme of bool * qualid or_by_notation * sort_expr - | CaseScheme of bool * qualid or_by_notation * sort_expr + | InductionScheme of bool * qualid or_by_notation * Sorts.family + | CaseScheme of bool * qualid or_by_notation * Sorts.family | EqualityScheme of qualid or_by_notation type section_subset_expr = |