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 /engine/termops.mli | |
| parent | d403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (diff) | |
| parent | 17b620f8bdf47a744d24513dcaef720d9160d443 (diff) | |
Merge PR #890: Global universe declarations
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index c9a530076c..c1600abe80 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -271,6 +271,8 @@ val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference + (** Combinators on judgments *) val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment |