Commit 935f9cf7 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'bugfix/v0.87'

parents 21cfdfc8 af22e5a8
......@@ -1712,12 +1712,12 @@ BNF = qualid label constant operator term type formula theory theory2 \
why_file spec expr expr2 module whyml_file term_old_at
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
doc/%_bnf.tex: doc/%.bnf doc/bnf
doc/bnf $< > $@
doc/%_bnf.tex: doc/%.bnf doc/bnf$(EXE)
doc/bnf$(EXE) $< > $@
doc/bnf: doc/bnf.mll
doc/bnf$(EXE): doc/bnf.mll
$(OCAMLLEX) $<
$(OCAMLOPT) -o $@ doc/bnf.ml
$(OCAMLC) -o $@ doc/bnf.ml
DOC = api glossary ide intro exec macros manpages install \
manual starting syntax syntaxref technical version whyml \
......@@ -1728,6 +1728,9 @@ DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib share/provers-detection-data.conf
cd doc; $(RUBBER) --warn all --pdf manual.tex
CLEANDIRS += doc
GENERATED += doc/bnf.ml
ifeq (@enable_html_doc@,yes)
# the dependency on the pdf ensures the bbl was built
......@@ -1746,7 +1749,8 @@ doc/html/index.html:
endif
clean::
cd doc; rm -rf html; $(RUBBER) --pdf --clean manual.tex
rm -rf doc/bnf$(EXE) $(BNFTEX) doc/html doc/manual.image.out; \
cd doc; $(RUBBER) --pdf --clean manual.tex
else
......@@ -1830,6 +1834,7 @@ STDLIBS = algebra \
bag \
bintree \
bool \
bv \
floating_point \
graph \
int \
......@@ -1837,16 +1842,24 @@ STDLIBS = algebra \
map \
number \
option \
seq \
pigeon \
real \
relations \
seq \
set \
sum \
bv
sum
# function ? tptp ?
STDMODS = array matrix hashtbl impset pqueue queue random ref stack string
STDMODS = array \
hashtbl \
impset \
matrix \
pqueue \
queue \
random \
ref \
stack \
string
STDMACS = array int
......@@ -1878,11 +1891,11 @@ clean::
%.cmi: %.mli
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
# supress "unused rec" warning for Menhir-produced files
# suppress "unused rec" warning for Menhir-produced files
%.cmo: %.ml %.mly
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) -w -39 $<
# supress "unused rec" warning for Menhir-produced files
# suppress "unused rec" warning for Menhir-produced files
%.cmx: %.ml %.mly
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) -w -39 $<
......@@ -2042,7 +2055,8 @@ configure: configure.in Version
distclean: clean
rm -f config.status config.cache config.log .merlin \
Makefile src/util/config.ml doc/version.tex
Makefile src/util/config.ml doc/version.tex \
src/jessie/Makefile src/config.sh lib/why3/META
depend:
rm -f $^
......
......@@ -31,19 +31,19 @@ let lt_nat x y = le zero y && lt x y
let lex (x1,x2) (y1,y2) = lt x1 y1 || eq x1 y1 && lt x2 y2
let euclidean_div_mod x y =
if eq y zero then zero, zero else quomod_big_int x y
if sign y = 0 then zero, zero else quomod_big_int x y
let euclidean_div x y = fst (euclidean_div_mod x y)
let euclidean_mod x y = snd (euclidean_div_mod x y)
let computer_div_mod x y =
let q,r = euclidean_div_mod x y in
let (q,r) as qr = euclidean_div_mod x y in
(* when y <> 0, we have x = q*y + r with 0 <= r < |y| *)
if sign x < 0 then
if sign x >= 0 || sign r = 0 then qr
else
if sign y < 0
then (pred q, add r y)
else (succ q, sub r y)
else (q,r)
let computer_div x y = fst (computer_div_mod x y)
let computer_mod x y = snd (computer_div_mod x y)
......
......@@ -136,7 +136,7 @@
(indent-line-to cur-indent)
(indent-line-to 0)))))))
; compile will propose "why3 ide file" is no Makefile is present
; compile will propose "why3 ide file" if no Makefile is present
(add-hook 'why3-mode-hook
(lambda ()
......
......@@ -37,15 +37,15 @@ let gt = gt_big_int
let le = le_big_int
let ge = ge_big_int
let euclidean_div_mod = quomod_big_int
let euclidean_div_mod x y =
if sign y = 0 then zero, zero else quomod_big_int x y
let euclidean_div x y = fst (euclidean_div_mod x y)
let euclidean_mod x y = snd (euclidean_div_mod x y)
let computer_div_mod x y =
let (q,r) as qr = quomod_big_int x y in
(* we have x = q*y + r with 0 <= r < |y| *)
let (q,r) as qr = euclidean_div_mod x y in
(* when y <> 0, we have x = q*y + r with 0 <= r < |y| *)
if sign x >= 0 || sign r = 0 then qr
else
if sign y < 0
......@@ -53,7 +53,6 @@ let computer_div_mod x y =
else (succ q, sub r y)
let computer_div x y = fst (computer_div_mod x y)
let computer_mod x y = snd (computer_div_mod x y)
let min = min_big_int
......
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