diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
| commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
| tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /backend/Inlining.v | |
| parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
| parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
| download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip | |
Merge branch 'master' into merge_master_8.13.1
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
Diffstat (limited to 'backend/Inlining.v')
| -rw-r--r-- | backend/Inlining.v | 14 |
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 := |