bump riscv-coq

mit-plv · Nov 8, 2020 · 13365e8 · 13365e8
1 parent 679f441
commit 13365e8
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/compiler/src/compiler/Softmul.v b/compiler/src/compiler/Softmul.v
@@ -240,6 +240,7 @@ Section Riscv.
     - simp. rewrite Hp4 in E. rewrite map.get_empty in E. discriminate E.
     - eauto 10.
     - simp. eauto 10.
+    - simp. eauto 10.
     - exists initialH.
       intuition (congruence || eauto 10).
     - eexists. ssplit; cycle -1. 1: eassumption. all: record.simp; try congruence. eauto 10.

diff --git a/deps/riscv-coq b/deps/riscv-coq
+1 −1		deps/riscv-semantics
+3 −29		src/riscv/Examples/WMM.v
+7 −1		src/riscv/Examples/WMMFree.v
+5 −4		src/riscv/Platform/AtomicMinimal.v
+1 −0		src/riscv/Platform/LogInstructionTrace.v
+3 −0		src/riscv/Platform/MaterializeRiscvProgram.v
+1 −0		src/riscv/Platform/MetricMinimal.v
+1 −0		src/riscv/Platform/MetricMinimalMMIO.v
+1 −0		src/riscv/Platform/MetricSane.v
+1 −0		src/riscv/Platform/Minimal.v
+1 −0		src/riscv/Platform/MinimalCSRs.v
+1 −0		src/riscv/Platform/MinimalCSRsDet.v
+1 −0		src/riscv/Platform/MinimalLogging.v
+1 −0		src/riscv/Platform/MinimalMMIO.v
+1 −0		src/riscv/Platform/MinimalMMIO_Post.v
+10 −10		src/riscv/Spec/ExecuteI.v
+1 −0		src/riscv/Spec/Machine.v
+1 −0		src/riscv/Spec/MetricPrimitives.v
+1 −0		src/riscv/Spec/Primitives.v