Merge pull request #1066 from MetaCoq/fix-letin-inline-reorder

Fix inlining and reorder constructors which were not translating let …
MetaCoq · Mar 8, 2024 · dfea0a5 · dfea0a5
2 parents 6037418 + 690e443
commit dfea0a5
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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