diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 7fef95f17b..3ae6e586c1 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -246,7 +246,7 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located (** Convenience function. Wrapper around {!find} to recover the source of an evar in a given evar map. *) -val evar_ident : existential_key -> evar_map -> Id.t +val evar_ident : existential_key -> evar_map -> Id.t option val rename : existential_key -> Id.t -> evar_map -> evar_map @@ -451,6 +451,7 @@ val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map val undefined_metas : evar_map -> metavariable list val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map +val map_metas : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status @@ -503,9 +504,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map @@ -540,10 +541,10 @@ val universes : evar_map -> UGraph.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_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map -val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a +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 @@ -558,12 +559,12 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts -val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant -val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts +val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> +val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** @@ -596,6 +597,8 @@ type unsolvability_explanation = SeveralInstancesFound of int val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds +val pr_evar_suggested_name : existential_key -> evar_map -> Id.t + (** {5 Debug pretty-printers} *) val pr_evar_info : evar_info -> Pp.std_ppcmds |