diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
commit | a36b3b755e25b8c5d61b9e069114858d9b768f04 (patch) | |
tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /cparser/validator/Interpreter_complete.v | |
parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
download | compcert-a36b3b755e25b8c5d61b9e069114858d9b768f04.tar.gz compcert-a36b3b755e25b8c5d61b9e069114858d9b768f04.zip |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'cparser/validator/Interpreter_complete.v')
-rw-r--r-- | cparser/validator/Interpreter_complete.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index ff88571b..f76731d5 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -304,7 +304,7 @@ reflexivity. destruct p. reflexivity. simpl; rewrite build_pt_dot_cost. -simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity. +simpl; rewrite <- plus_n_Sm, Nat.add_assoc; reflexivity. Qed. Lemma build_pt_dot_buffer: @@ -593,12 +593,12 @@ Lemma parse_fix_complete: Proof. fix 3. destruct n_steps; intros; simpl. -apply lt_0_Sn. +apply Nat.lt_0_succ. apply step_next_ptd in H. pose proof (next_ptd_cost ptd). destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition. rewrite H3 in H0; rewrite H0. -apply le_n_S, le_0_n. +apply le_n_S, Nat.le_0_l. destruct (next_ptd ptd); intuition; subst. eapply parse_fix_complete with (n_steps:=n_steps) in H1. rewrite H0. @@ -648,7 +648,7 @@ generalize (start_nt init). dependent destruction full_pt0. intros. rewrite build_pt_dot_cost; simpl. -rewrite H, plus_0_r; reflexivity. +rewrite H, Nat.add_0_r; reflexivity. Qed. Lemma init_ptd_buffer: |