summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-02-24 12:44:00 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-02-24 12:44:00 +0000
commit795ba8abf7d77f5edd2bce83e0b5322acb68f488 (patch)
tree63b6e716f2bb79f3d331381d26139dfb127543b2
parentd520510710146fba42d5e545315a98363f121758 (diff)
Silence the warning "Cannot build inversion information".
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--lib/Parmov.v19
1 files changed, 10 insertions, 9 deletions
diff --git a/lib/Parmov.v b/lib/Parmov.v
index fb04310..f96a692 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -950,7 +950,7 @@ Qed.
and returns a sequence of elementary moves [tau] that is semantically
equivalent. We start by defining a number of auxiliary functions. *)
-Function split_move (m: moves) (r: reg) {struct m} : option (moves * reg * moves) :=
+Fixpoint split_move (m: moves) (r: reg) {struct m} : option (moves * reg * moves) :=
match m with
| nil => None
| (s, d) :: tl =>
@@ -962,7 +962,7 @@ Function split_move (m: moves) (r: reg) {struct m} : option (moves * reg * moves
end
end.
-Function is_last_source (r: reg) (m: moves) {struct m} : bool :=
+Fixpoint is_last_source (r: reg) (m: moves) {struct m} : bool :=
match m with
| nil => false
| (s, d) :: nil =>
@@ -971,7 +971,7 @@ Function is_last_source (r: reg) (m: moves) {struct m} : bool :=
is_last_source r tl
end.
-Function replace_last_source (r: reg) (m: moves) {struct m} : moves :=
+Fixpoint replace_last_source (r: reg) (m: moves) {struct m} : moves :=
match m with
| nil => nil
| (s, d) :: nil => (r, d) :: nil
@@ -1015,12 +1015,13 @@ Lemma split_move_charact:
| None => no_read m r
end.
Proof.
- unfold no_read. intros m r. functional induction (split_move m r).
- red; simpl. tauto.
- split. reflexivity. simpl; auto.
- rewrite e1 in IHo. simpl. intuition.
- rewrite e1 in IHo. destruct IHo. split. rewrite H. reflexivity.
- simpl. intuition.
+ unfold no_read. induction m; simpl; intros.
+- tauto.
+- destruct a as [s d]. destruct (reg_eq s r).
+ + subst s. auto.
+ + specialize (IHm r). destruct (split_move m r) as [[[before d'] after] | ].
+ * destruct IHm. subst m. simpl. intuition.
+ * simpl; intuition.
Qed.
Lemma is_last_source_charact: