From 2638a022276c932ed00dc3f64b0e58bc0114a3d7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 12:55:03 +0100 Subject: la division flottante fonctionne --- backend/SelectDivproof.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backend/SelectDivproof.v') diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 9b99fcbf..dbd3f58d 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -949,8 +949,8 @@ Proof. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. - + TrivialExists. -- TrivialExists. + + apply eval_divf_base; trivial. +- apply eval_divf_base; trivial. Qed. Theorem eval_divfs: @@ -965,8 +965,8 @@ Proof. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. destruct x; simpl; auto. erewrite Float32.div_mul_inverse; eauto. - + TrivialExists. -- TrivialExists. + + apply eval_divfs_base; trivial. +- apply eval_divfs_base; trivial. Qed. End CMCONSTRS. -- cgit