1 files changed, 4 insertions, 1 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 1d13702a..1d713010 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -969,7 +969,10 @@ Theorem eval_platform_builtin:
   platform_builtin_sem bf vl = Some v ->
   exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
 Proof.
-  intros. discriminate.
+  destruct bf; intros until le; intro Heval.
+  all: try (inversion Heval; subst a; clear Heval;
+       exists v; split; trivial;
+       repeat (try econstructor; try eassumption)).
 Qed.
 
 End CMCONSTR.