workaround needed because itauto lia seems to unfold definitions

See https://gitlab.inria.fr/fbesson/itauto/-/issues/2
mit-plv · Aug 27, 2020 · b521386 · b521386
1 parent 5316184
commit b521386
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/compiler/src/compilerExamples/FibCompiled.v b/compiler/src/compilerExamples/FibCompiled.v
@@ -116,7 +116,7 @@ Section FibCompiled.
       apply Nat.lt_le_pred in H.
       simpl in H.
       specialize (Hinc H).
-      bomega.
+      Lia.lia.
   Qed.
 
   Local Notation instructionsH := (bedrock2.MetricLogging.instructions).

diff --git a/end2end/src/end2end/End2EndLightbulb.v b/end2end/src/end2end/End2EndLightbulb.v
@@ -281,8 +281,9 @@ Proof.
       }
       SeparationLogic.seprewrite_in @Array.bytearray_append Hr.
       SeparationLogic.seprewrite_in @SeparationLogic.sep_emp_True_r Hr0.
-      eexists _, _; split;
-        [exact Hr1|rewrite List.length_firstn_inbounds; blia]. }
+      eexists _, _; split; [exact Hr1|].
+      clear -Hl.
+      rewrite List.length_firstn_inbounds; blia. }
     subst a; rewrite app_nil_r.
     eexists; split; eauto.
     change x0 with (List.app nil x0).