aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inlining.v
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
commitf16fa31ec9cc90da750c8cc10f447023962cd153 (patch)
tree28eed4d4b5bc964907f20332d1eed470a393d07b /backend/Inlining.v
parent485a4c0dd450e65745c83e59acdb40b42058e556 (diff)
parentd703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e (diff)
downloadcompcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.tar.gz
compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.zip
Merge branch 'kvx-work' into BTL
Diffstat (limited to 'backend/Inlining.v')
-rw-r--r--backend/Inlining.v14
1 files changed, 7 insertions, 7 deletions
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 8c7e1898..0e18d38e 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -71,12 +71,12 @@ Inductive sincr (s1 s2: state) : Prop :=
Remark sincr_refl: forall s, sincr s s.
Proof.
- intros; constructor; xomega.
+ intros; constructor; extlia.
Qed.
Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3.
Proof.
- intros. inv H; inv H0. constructor; xomega.
+ intros. inv H; inv H0. constructor; extlia.
Qed.
(** Dependently-typed state monad, ensuring that the final state is
@@ -111,7 +111,7 @@ Program Definition set_instr (pc: node) (i: instruction): mon unit :=
(mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize))
_.
Next Obligation.
- intros; constructor; simpl; xomega.
+ intros; constructor; simpl; extlia.
Qed.
Program Definition add_instr (i: instruction): mon node :=
@@ -121,7 +121,7 @@ Program Definition add_instr (i: instruction): mon node :=
(mkstate s.(st_nextreg) (Pos.succ pc) (PTree.set pc i s.(st_code)) s.(st_stksize))
_.
Next Obligation.
- intros; constructor; simpl; xomega.
+ intros; constructor; simpl; extlia.
Qed.
Program Definition reserve_nodes (numnodes: positive): mon positive :=
@@ -130,7 +130,7 @@ Program Definition reserve_nodes (numnodes: positive): mon positive :=
(mkstate s.(st_nextreg) (Pos.add s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize))
_.
Next Obligation.
- intros; constructor; simpl; xomega.
+ intros; constructor; simpl; extlia.
Qed.
Program Definition reserve_regs (numregs: positive): mon positive :=
@@ -139,7 +139,7 @@ Program Definition reserve_regs (numregs: positive): mon positive :=
(mkstate (Pos.add s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize))
_.
Next Obligation.
- intros; constructor; simpl; xomega.
+ intros; constructor; simpl; extlia.
Qed.
Program Definition request_stack (sz: Z): mon unit :=
@@ -148,7 +148,7 @@ Program Definition request_stack (sz: Z): mon unit :=
(mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Z.max s.(st_stksize) sz))
_.
Next Obligation.
- intros; constructor; simpl; xomega.
+ intros; constructor; simpl; extlia.
Qed.
Program Definition ptree_mfold {A: Type} (f: positive -> A -> mon unit) (t: PTree.t A): mon unit :=