diff options
Diffstat (limited to 'kernel/vars.mli')
| -rw-r--r-- | kernel/vars.mli | 31 |
1 files changed, 14 insertions, 17 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli index 574d50ec..a0c7ba4b 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -11,10 +13,10 @@ open Constr (** {6 Occur checks } *) -(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) +(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *) val closedn : int -> constr -> bool -(** [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *) val closed0 : constr -> bool (** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *) @@ -73,6 +75,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl (** For compatibility: returns the substitution reversed *) val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list +(** Take an index in an instance of a context and returns its index wrt to + the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) +val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int + (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if @@ -125,20 +131,11 @@ val subst_var : Id.t -> constr -> constr open Univ -val subst_univs_fn_constr : universe_subst_fn -> constr -> constr -val subst_univs_fn_puniverses : universe_level_subst_fn -> - 'a puniverses -> 'a puniverses - -val subst_univs_constr : universe_subst -> constr -> constr - (** Level substitutions for polymorphism. *) val subst_univs_level_constr : universe_level_subst -> constr -> constr val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t (** Instance substitution for polymorphism. *) -val subst_instance_constr : universe_instance -> constr -> constr -val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t - -type id_key = constant tableKey -val eq_id_key : id_key -> id_key -> bool +val subst_instance_constr : Instance.t -> constr -> constr +val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t |