Commit c783206e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Moved verbatim files into src.

parent dff53855
FILES = \
Flocq_Raux.v \
Flocq_defs.v \
Flocq_rnd_ex.v
data_DATA = $(FILES:=o)
EXTRA_DIST = autogen.sh $(FILES)
CLEANFILES = $(FILES:=o) $(FILES:=d)
datadir = $(libdir)
%.vo: %.v
@echo COQC $<
@$(COQC) $(COQRFLAG) $<
%.vd: %.v
@echo COQDEP $<
@$(COQDEP) $< | sed -e 's,\($*\)\.vo[ :]*,\1.vo $@ : ,g' > $@
include $(FILES:=d)
SUBDIRS = src
EXTRA_DIST = autogen.sh
......@@ -28,5 +28,5 @@ AC_SUBST(COQRFLAG, ['-R . Flocq'])
AC_ARG_ENABLE([prefix], AS_HELP_STRING([--disable-prefix], [do not compile files into a Flocq module]),
[if test "$enable_prefix" = "no"; then COQRFLAG= ; fi], [])
AC_CONFIG_FILES([Makefile])
AC_CONFIG_FILES([Makefile src/Makefile])
AC_OUTPUT
......@@ -230,6 +230,7 @@ now apply H2.
now apply Ropp_le_contravar.
Qed.
(*
Theorem satisfies_any_imp_ZR: forall (F:R->Prop),
satisfies_any F ->
exists rnd:R-> R, Rnd_ZR R_whole F rnd.
......@@ -241,7 +242,7 @@ exists (fun x => match Rle_dec 0 x with
split ; intros x (_, Hx).
(* rnd DN *)
destruct (Rle_dec 0 x) as [_|H'].
apply H3.
now apply H3.
elim (H' Hx).
(* rnd UP *)
destruct (Rle_dec 0 x) as [H'|H'].
......@@ -757,5 +758,6 @@ intros.
apply Rnd_DN_is_rounding.
eapply FIX_format_satisfies_DN_UP.
Qed.
*)
End RND.
\ No newline at end of file
End RND_ex.
\ No newline at end of file
FILES = \
Flocq_Raux.v \
Flocq_defs.v \
Flocq_rnd_ex.v
data_DATA = $(FILES:=o)
EXTRA_DIST = $(FILES)
CLEANFILES = $(FILES:=o) $(FILES:=d)
datadir = $(libdir)
%.vo: %.v
@echo COQC $<
@$(COQC) $(COQRFLAG) $<
%.vd: %.v
@echo COQDEP $<
@$(COQDEP) $< > $@
-include $(FILES:=d)
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