Skip to content

GitLab

Commit bc865be2 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

fix admit

parent 63ddeebc
Show whitespace changes
Inline Side-by-side
riscV/RTLpathSE_simplify.v
View file @ bc865be2
......@@ -1955,8 +1955,7 @@ Proof.
- eapply simplify_ccompfs_correct; eauto.
(* Cnotcompfs *)
- eapply simplify_cnotcompfs_correct; eauto.
(*Qed.*)
Admitted.
Qed.
Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
(TARGET: target_cbranch_expanse hst c l = Some (c', l'))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment