diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 03:26:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 01:13:04 +0200 |
| commit | a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f (patch) | |
| tree | 911c09c586a6d90a6d1e304e86260767a7b0bdbb /interp | |
| 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 'interp')
| -rw-r--r-- | interp/constrextern.mli | 1 | ||||
| -rw-r--r-- | interp/constrintern.ml | 18 | ||||
| -rw-r--r-- | interp/declare.mli | 2 |
3 files changed, 10 insertions, 11 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 6f5887ca2..73c108319 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -18,7 +18,6 @@ open Pattern open Constrexpr open Notation_term open Notation -open Misctypes open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax diff --git a/interp/constrintern.ml b/interp/constrintern.ml index def8425ec..48f15f897 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -980,17 +980,17 @@ let intern_reference ref = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option = +let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option = match info with - | Misctypes.UAnonymous -> None - | Misctypes.UUnknown -> None - | Misctypes.UNamed id -> Some (id, 0) + | UAnonymous -> None + | UUnknown -> None + | UNamed id -> Some (id, 0) -let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = +let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | Misctypes.GProp -> Misctypes.GProp - | Misctypes.GSet -> Misctypes.GSet - | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] + | GProp -> GProp + | GSet -> GSet + | GType info -> GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) let intern_qualid qid intern env ntnvars us args = @@ -1024,7 +1024,7 @@ let intern_qualid qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) diff --git a/interp/declare.mli b/interp/declare.mli index f8cffbb1e..de4d8346a 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -88,5 +88,5 @@ val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> Misctypes.lident list -> unit -val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> +val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit |