diff options
| author | Pierre-Marie Pédrot | 2018-05-22 17:22:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-22 17:22:52 +0200 |
| commit | c792c9fc500cbc1cab14271ebc6a98cd516451b3 (patch) | |
| tree | a3ef08574a31fe1eec2ac6a5194d667789c33625 /engine/evd.mli | |
| parent | c3838b204d3db7a58246d960a3da7efb7d1cc2f2 (diff) | |
| parent | 748a33cee41900d285897b24b4d8e29dd9eb2a3d (diff) | |
Merge PR #7384: Split Universes
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 509db525d9..b2670ee518 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -354,7 +354,7 @@ val whd_sort_variable : evar_map -> econstr -> econstr exception UniversesDiffer -val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map +val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map (** Add the given universe unification constraints to the evar map. @raise UniversesDiffer in case a first-order unification fails. @raise UniverseInconsistency . @@ -543,14 +543,14 @@ val empty_evar_universe_context : UState.t val union_evar_universe_context : UState.t -> UState.t -> UState.t [@@ocaml.deprecated "Alias of UState.union"] -val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +val evar_universe_context_subst : UState.t -> UnivSubst.universe_opt_subst [@@ocaml.deprecated "Alias of UState.subst"] val constrain_variables : Univ.LSet.t -> UState.t -> UState.t [@@ocaml.deprecated "Alias of UState.constrain_variables"] val evar_universe_context_of_binders : - Universes.universe_binders -> UState.t + UnivNames.universe_binders -> UState.t [@@ocaml.deprecated "Alias of UState.of_binders"] val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t @@ -559,7 +559,7 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t -val universe_binders : evar_map -> Universes.universe_binders +val universe_binders : evar_map -> UnivNames.universe_binders val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t [@@ocaml.deprecated "Alias of UState.add_constraints"] @@ -603,7 +603,7 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t -val universe_subst : evar_map -> Universes.universe_opt_subst +val universe_subst : evar_map -> UnivSubst.universe_opt_subst val universes : evar_map -> UGraph.t (** [to_universe_context evm] extracts the local universes and @@ -622,7 +622,7 @@ val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map -val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map +val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a |