diff options
| author | Maxime Dénès | 2017-12-05 12:56:11 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-05 12:56:11 +0100 |
| commit | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (patch) | |
| tree | 1e8d3db28d8d19b575e9e555f6ce379960c842c1 /interp/declare.mli | |
| parent | d403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (diff) | |
| parent | 17b620f8bdf47a744d24513dcaef720d9160d443 (diff) | |
Merge PR #890: Global universe declarations
Diffstat (limited to 'interp/declare.mli')
| -rw-r--r-- | interp/declare.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/interp/declare.mli b/interp/declare.mli index d50d37368c..f368d164e9 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -80,13 +80,11 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool - - (** Global universe contexts, names and constraints *) +val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> - (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> - unit +val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit |