diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_subst.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 930d9aa7d..640aecb98 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -693,7 +693,7 @@ let occur_mbid uid = occur_uid (MBI uid) type 'a lazy_subst = | LSval of 'a - | LSlazy of substitution * 'a + | LSlazy of substitution list * 'a type 'a substituted = 'a lazy_subst ref @@ -703,14 +703,14 @@ let force fsubst r = match !r with | LSval a -> a | LSlazy(s,a) -> - let a' = fsubst s a in + let subst = List.fold_left join empty_subst (List.rev s) in + let a' = fsubst subst a in r := LSval a'; a' let subst_substituted s r = match !r with - | LSval a -> ref (LSlazy(s,a)) + | LSval a -> ref (LSlazy([s],a)) | LSlazy(s',a) -> - let s'' = join s' s in - ref (LSlazy(s'',a)) + ref (LSlazy(s::s',a)) |