diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 19:03:03 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 19:03:03 +0100 |
commit | ed0c434a05a929a659e43aed80ab7c8179a7daa3 (patch) | |
tree | d486bf54f6bbfd6ace8dc9cea52b959699f88ebe /engine | |
parent | c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (diff) |
[api] Insert miscellaneous API deprecation back to core.
Diffstat (limited to 'engine')
-rw-r--r-- | engine/evd.mli | 45 | ||||
-rw-r--r-- | engine/proofview.mli | 2 | ||||
-rw-r--r-- | engine/termops.mli | 3 |
3 files changed, 26 insertions, 24 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 45ca1a365..af5373582 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -125,6 +125,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) type evar_universe_context = UState.t +[@@ocaml.deprecated "Alias of UState.t"] (** The universe context associated to an evar map *) type evar_map @@ -138,7 +139,7 @@ val from_env : env -> evar_map (** The empty evar map with given universe context, taking its initial universes from env. *) -val from_ctx : evar_universe_context -> evar_map +val from_ctx : UState.t -> evar_map (** The empty evar map with given universe context *) val is_empty : evar_map -> bool @@ -486,37 +487,37 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -type 'a in_evar_universe_context = 'a * evar_universe_context +type 'a in_evar_universe_context = 'a * UState.t -val evar_universe_context_set : evar_universe_context -> Univ.ContextSet.t -val evar_universe_context_constraints : evar_universe_context -> Univ.constraints -val evar_context_universe_context : evar_universe_context -> Univ.UContext.t -val evar_universe_context_of : Univ.ContextSet.t -> evar_universe_context -val empty_evar_universe_context : evar_universe_context -val union_evar_universe_context : evar_universe_context -> evar_universe_context -> - evar_universe_context -val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context +val evar_universe_context_set : UState.t -> Univ.ContextSet.t +val evar_universe_context_constraints : UState.t -> Univ.constraints +val evar_context_universe_context : UState.t -> Univ.UContext.t +val evar_universe_context_of : Univ.ContextSet.t -> UState.t +val empty_evar_universe_context : UState.t +val union_evar_universe_context : UState.t -> UState.t -> + UState.t +val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : - Universes.universe_binders -> evar_universe_context + Universes.universe_binders -> UState.t -val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context +val make_evar_universe_context : env -> (Id.t located) list option -> UState.t 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 -> string -> Univ.Level.t val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map -val add_constraints_context : evar_universe_context -> - Univ.constraints -> evar_universe_context +val add_constraints_context : UState.t -> + Univ.constraints -> UState.t -val normalize_evar_universe_context_variables : evar_universe_context -> +val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context -val normalize_evar_universe_context : evar_universe_context -> - evar_universe_context +val normalize_evar_universe_context : UState.t -> + UState.t val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -548,7 +549,7 @@ val set_eq_instances : ?flex:bool -> val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool -val evar_universe_context : evar_map -> evar_universe_context +val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> (Id.t * Univ.Level.t) list * Univ.UContext.t @@ -558,8 +559,8 @@ val universes : evar_map -> UGraph.t val check_univ_decl : evar_map -> UState.universe_decl -> Universes.universe_binders * Univ.UContext.t -val merge_universe_context : evar_map -> evar_universe_context -> evar_map -val set_universe_context : evar_map -> evar_universe_context -> evar_map +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 @@ -567,7 +568,7 @@ val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst -val abstract_undefined_variables : evar_universe_context -> evar_universe_context +val abstract_undefined_variables : UState.t -> UState.t val fix_undefined_variables : evar_map -> evar_map diff --git a/engine/proofview.mli b/engine/proofview.mli index d92d0a7d5..0379d4b49 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -426,7 +426,7 @@ module Unsafe : sig val tclGETGOALS : Evd.evar list tactic (** Sets the evar universe context. *) - val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic + val tclEVARUNIVCONTEXT : UState.t -> unit tactic (** Clears the future goals store in the proof view. *) val reset_future_goals : proofview -> proofview diff --git a/engine/termops.mli b/engine/termops.mli index 2dab0685d..793490798 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -113,6 +113,7 @@ val collect_metas : Evd.evar_map -> constr -> int list val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *) +[@@ocaml.deprecated "alias of Termops.dependent"] (* Substitution of metavariables *) type meta_value_map = (metavariable * Constr.constr) list @@ -290,7 +291,7 @@ val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> evar_map -> Pp.t val pr_metaset : Metaset.t -> Pp.t -val pr_evar_universe_context : evar_universe_context -> Pp.t +val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t (** debug printer: do not use to display terms to the casual user... *) |