diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /interp/declare.ml | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 0ead94effe..0cc4d0fcaa 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -15,7 +15,7 @@ open Names open Libnames open Globnames open Nameops -open Term +open Constr open Declarations open Entries open Libobject @@ -440,7 +440,7 @@ let assumption_message id = (** Global universe names, in a different summary *) -type universe_context_decl = polymorphic * Univ.universe_context_set +type universe_context_decl = polymorphic * Univ.ContextSet.t let cache_universe_context (p, ctx) = Global.push_context_set p ctx; @@ -458,7 +458,7 @@ let declare_universe_context poly ctx = Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) (* Discharged or not *) -type universe_decl = polymorphic * (Id.t * Univ.universe_level) list +type universe_decl = polymorphic * (Id.t * Univ.Level.t) list let cache_universes (p, l) = let glob = Global.global_universe_names () in |