diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:05:56 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:05:56 +0000 |
| commit | 6946bbbf2390024b3ded7654814104e709cce755 (patch) | |
| tree | 643429de27ef09026b937c18a55075eb49b11fee /kernel/mod_subst.mli | |
| parent | aa37087b8e7151ea96321a11012c1064210ef4ea (diff) | |
Modulification of mod_bound_id
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |