Mod_subst.force: avoid using join when only one subst

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16381 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 4 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 335aba520..af8b1f217 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -464,10 +464,13 @@ let force fsubst r =
   match !r with
   | LSval a -> a
   | LSlazy(s,a) ->
-      let subst = List.fold_left join empty_subst (List.rev s) in
-      let a' = fsubst subst a in
-      r := LSval a';
-      a'
+    match List.rev s with
+      | [] -> assert false
+      | sub0::subs ->
+        let subst = List.fold_left join sub0 subs in
+        let a' = fsubst subst a in
+        r := LSval a';
+        a'
 
 let subst_substituted s r =
   match !r with