diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-17 18:28:55 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-17 18:28:55 +0100 |
| commit | a1c401a4eba5fc9fcf42933f70005ecb679a4c1c (patch) | |
| tree | 26637fca5d1da9b3d049234721d593a60b03a6d3 /backend/CminorSel.v | |
| parent | c49caca4b5f0239b43610fbfe012d6ba0211b364 (diff) | |
| parent | 1daf96cdca4d828c333cea5c9a314ef861342984 (diff) | |
| download | compcert-dev/michalis.tar.gz compcert-dev/michalis.zip | |
Merge branch 'master' into dev/michalisdev/michalis
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 96cb8ae6..f6f6e34d 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. |