diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/API/API.mli b/API/API.mli index 889050d90a..5c78606715 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2881,12 +2881,12 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - Univ.UContext.t val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map + val to_universe_context : evar_map -> Univ.UContext.t + val meta_list : evar_map -> (Constr.metavariable * clbinding) list val meta_defined : evar_map -> Constr.metavariable -> bool |