From 6946bbbf2390024b3ded7654814104e709cce755 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 18 Dec 2012 18:05:56 +0000 Subject: Modulification of mod_bound_id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_subst.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/mod_subst.mli') diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 21b6bf93b..f3c490652 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -62,13 +62,13 @@ val is_empty_subst : substitution -> bool (** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential composition *) val add_mbid : - mod_bound_id -> module_path -> delta_resolver -> substitution -> substitution + MBId.t -> module_path -> delta_resolver -> substitution -> substitution val add_mp : module_path -> module_path -> delta_resolver -> substitution -> substitution (** map_* create a new substitution [arg2/arg1]\{arg3\} *) val map_mbid : - mod_bound_id -> module_path -> delta_resolver -> substitution + MBId.t -> module_path -> delta_resolver -> substitution val map_mp : module_path -> module_path -> delta_resolver -> substitution @@ -136,7 +136,7 @@ val subst_mps : substitution -> constr -> constr (** [occur_*id id sub] returns true iff [id] occurs in [sub] on either side *) -val occur_mbid : mod_bound_id -> substitution -> bool +val occur_mbid : MBId.t -> substitution -> bool (** [repr_substituted r] dumps the representation of a substituted: - [None, a] when r is a value -- cgit v1.2.3