diff options
| author | glondu | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /kernel/mod_subst.mli | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 6ae9649d6b..d30168a1bf 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -20,9 +20,9 @@ val make_resolver : (constant * constr option) list -> resolver val empty_subst : substitution -val add_msid : +val add_msid : mod_self_id -> module_path -> substitution -> substitution -val add_mbid : +val add_mbid : mod_bound_id -> module_path -> resolver option -> substitution -> substitution val add_mp : module_path -> module_path -> substitution -> substitution @@ -34,7 +34,7 @@ val map_mbid : val map_mp : module_path -> module_path -> substitution -(* sequential composition: +(* sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] *) val join : substitution -> substitution -> substitution @@ -50,10 +50,10 @@ val debug_pr_subst : substitution -> Pp.std_ppcmds (*i*) (* [subst_mp sub mp] guarantees that whenever the result of the - substitution is structutally equal [mp], it is equal by pointers - as well [==] *) + substitution is structutally equal [mp], it is equal by pointers + as well [==] *) -val subst_mp : +val subst_mp : substitution -> module_path -> module_path val subst_kn : @@ -77,7 +77,7 @@ val replace_mp_in_con : module_path -> module_path -> constant -> constant names appearing in [c] *) val subst_mps : substitution -> constr -> constr -(* [occur_*id id sub] returns true iff [id] occurs in [sub] +(* [occur_*id id sub] returns true iff [id] occurs in [sub] on either side *) val occur_msid : mod_self_id -> substitution -> bool |