Commit bb571876 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Name change

parent 718b6d16
...@@ -35,3 +35,6 @@ Theorem Axpy_opt : ...@@ -35,3 +35,6 @@ Theorem Axpy_opt :
bpow (1-prec) / (6*bpow 1) * Rabs y)%R -> bpow (1-prec) / (6*bpow 1) * Rabs y)%R ->
(MinOrMax (a1 * x1 + y1) u). (MinOrMax (a1 * x1 + y1) u).
Admitted. Admitted.
End Axpy.
\ No newline at end of file
...@@ -22,7 +22,8 @@ FILES = \ ...@@ -22,7 +22,8 @@ FILES = \
Prop/Fprop_plus_error.v \ Prop/Fprop_plus_error.v \
Prop/Fprop_relative.v \ Prop/Fprop_relative.v \
Prop/Fprop_div_sqrt_error.v \ Prop/Fprop_div_sqrt_error.v \
Prop/Fprop_Sterbenz.v Prop/Fprop_Sterbenz.v \
Appli/Fappli_Axpy.v
EXTRA_DIST = $(FILES) EXTRA_DIST = $(FILES)
CLEANFILES = $(FILES:=o) $(FILES:=d) $(FILES:.v=.glob) CLEANFILES = $(FILES:=o) $(FILES:=d) $(FILES:.v=.glob)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment