diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-10 18:28:26 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-10 18:28:26 +0200 |
commit | f16fa31ec9cc90da750c8cc10f447023962cd153 (patch) | |
tree | 28eed4d4b5bc964907f20332d1eed470a393d07b /backend/CminorSel.v | |
parent | 485a4c0dd450e65745c83e59acdb40b42058e556 (diff) | |
parent | d703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e (diff) | |
download | compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.tar.gz compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.zip |
Merge branch 'kvx-work' into BTL
Diffstat (limited to 'backend/CminorSel.v')
-rw-r--r-- | backend/CminorSel.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 26f47e23..cedd2bed 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -464,7 +464,7 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). -Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. +Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. (** * Lifting of let-bound variables *) @@ -522,9 +522,9 @@ Lemma insert_lenv_lookup1: nth_error le' n = Some v. Proof. induction 1; intros. - omegaContradiction. + extlia. destruct n; simpl; simpl in H0. auto. - apply IHinsert_lenv. auto. omega. + apply IHinsert_lenv. auto. lia. Qed. Lemma insert_lenv_lookup2: @@ -536,8 +536,8 @@ Lemma insert_lenv_lookup2: Proof. induction 1; intros. simpl. assumption. - simpl. destruct n. omegaContradiction. - apply IHinsert_lenv. exact H0. omega. + simpl. destruct n. extlia. + apply IHinsert_lenv. exact H0. lia. Qed. Lemma eval_lift_expr: @@ -580,4 +580,4 @@ Proof. eexact H. apply insert_lenv_0. Qed. -Hint Resolve eval_lift: evalexpr. +Global Hint Resolve eval_lift: evalexpr. |