From 5635c35ea4ec172fd81147effed4f33e2f581aaa Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 2 Apr 2013 22:08:30 +0000 Subject: 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 --- checker/declarations.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'checker/declarations.ml') 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 -- cgit v1.2.3