diff --git a/erasure/theories/EInlining.v b/erasure/theories/EInlining.v
index 529e5f9ff..caff8e359 100644
--- a/erasure/theories/EInlining.v
+++ b/erasure/theories/EInlining.v
@@ -21,7 +21,7 @@ Section Inline.
   Equations inline (t : term) : term :=
     | tVar na => tVar na
     | tLambda nm bod => tLambda nm (inline bod)
-    | tLetIn nm dfn bod => tLetIn nm dfn bod
+    | tLetIn nm dfn bod => tLetIn nm (inline dfn) (inline bod)
     | tApp fn arg => tApp (inline fn) (inline arg)
     | tConst nm with KernameMap.find nm inlining :=
       { | Some body := (* Already inlined body *) body
diff --git a/erasure/theories/EReorderCstrs.v b/erasure/theories/EReorderCstrs.v
index 071d6b57a..3e029f23e 100644
--- a/erasure/theories/EReorderCstrs.v
+++ b/erasure/theories/EReorderCstrs.v
@@ -48,7 +48,7 @@ Section Reorder.
   Equations reorder (t : term) : term :=
     | tVar na => tVar na
     | tLambda nm bod => tLambda nm (reorder bod)
-    | tLetIn nm dfn bod => tLetIn nm dfn bod
+    | tLetIn nm dfn bod => tLetIn nm (reorder dfn) (reorder bod)
     | tApp fn arg => tApp (reorder fn) (reorder arg)
     | tConst nm => tConst nm
     | tConstruct i m args => tConstruct i (lookup_constructor_ordinal i m) (map reorder args)
diff --git a/make-opam-files.sh b/make-opam-files.sh
index 1de13c702..2d88765ce 100755
--- a/make-opam-files.sh
+++ b/make-opam-files.sh
@@ -21,7 +21,7 @@ do
     opamf=${f/.opam/};
     target=$1/$opamf/$opamf.$2/opam;
     echo $opamf;
-    mkdir $1/$opamf/$opamf.$2
+    mkdir -p $1/$opamf/$opamf.$2
     gsed -e "/^version:.*/d" $f > $target
     echo url { >> $target
     echo "  src:" \"$3\" >> $target