diff --git a/Makefile.in b/Makefile.in
index e2bfbee05678b612d2cd429ef1af6e19e7111af9..66dc042e6ed52c072c0f585affb346c66ef8c15b 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -986,8 +986,9 @@ COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
endif
COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision
+COQLIBS_FOR_DRIVERS = $(addprefix lib/coq/for_drivers/, $(COQLIBS_FOR_DRIVERS_FILES))
-COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT)
+COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) $(COQLIBS_FOR_DRIVERS)
%.vo: %.v
$(SHOW) 'Coqc $<'
@@ -1035,8 +1036,8 @@ drivers/coq-realizations.aux: Makefile
echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
- for f in $(COQLIBS_FOR_DRIVER_FILES); do \
- echo 'theory for_driver.'"$$f"' meta "realized_theory" "for_driver.'"$$f"'", "" end'; done; \
+ for f in $(COQLIBS_FOR_DRIVERS_FILES); do \
+ echo 'theory for_drivers.'"$$f"' meta "realized_theory" "for_drivers.'"$$f"'", "" end'; done; \
) > $@
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-bv update-coq-ieee_float update-coq-for-drivers
@@ -1110,6 +1111,8 @@ ifeq (@enable_coq_fp_libs@,yes)
$(MKDIR_P) $(LIBDIR)/why3/coq/ieee_float
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
endif
+ $(MKDIR_P) $(LIBDIR)/why3/coq/for_drivers
+ $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FOR_DRIVERS)) $(LIBDIR)/why3/coq/for_drivers/
$(MKDIR_P) $(DATADIR)/why3/drivers
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
diff --git a/lib/coq/for_drivers/ComputerOfEuclideanDivision.v b/lib/coq/for_drivers/ComputerOfEuclideanDivision.v
index eb7a50aaa290b18eed0a44a09e4f5f8727bef3fe..5e9c74a4e132367761311a6bd3d8c0aa8c50e569 100644
--- a/lib/coq/for_drivers/ComputerOfEuclideanDivision.v
+++ b/lib/coq/for_drivers/ComputerOfEuclideanDivision.v
@@ -64,7 +64,6 @@ Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
(-d)%Z))%Z))))).
intros n d.
unfold int.EuclideanDivision.mod1.
- SearchAbout Z.rem Z.quot.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
assert (H:= Z.quot_rem' n d).
omega.
diff --git a/src/transform/abstract_quantifiers.ml b/src/transform/abstract_quantifiers.ml
index 4ae305ad3b03ce23ca0ab157013e4d6041a433ee..b6fc919f26997c975134d94b82d5cba4ee2d354b 100644
--- a/src/transform/abstract_quantifiers.ml
+++ b/src/transform/abstract_quantifiers.ml
@@ -24,13 +24,14 @@ let rec elim_quant pol f =
let elim_less (d:decl) =
match d.d_node with
- | Dprop (Paxiom,_v,t) ->
- let t = elim_quant true t in
- if t_equal t t_true then []
- else
- [decl_map (fun _ -> t) d]
+ | Dprop (p,_v,t) ->
+ let pol = match p with | Paxiom | Plemma -> true | Pgoal -> false in
+ let t = elim_quant pol t in
+ if p <> Pgoal && t_equal t t_true then []
+ else
+ [decl_map (fun _ -> t) d]
| _ -> [d]
let () =
Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None)
- ~desc:"abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context@."
+ ~desc:"abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context and the goals@."
diff --git a/why3-coq.opam/files/run_autoconf_if_needed.sh b/why3-coq.opam/files/run_autoconf_if_needed.sh
new file mode 100644
index 0000000000000000000000000000000000000000..afcace02492ef677436aa93d0fe781e4eea6338a
--- /dev/null
+++ b/why3-coq.opam/files/run_autoconf_if_needed.sh
@@ -0,0 +1,6 @@
+#!/bin/sh -eux
+
+if [ ! -f "configure" ]; then
+ autoconf
+ automake --add-missing || true
+fi
diff --git a/why3-coq.opam/opam b/why3-coq.opam/opam
index 361aac6a2bf28194b9f50b900b2a8990fc717826..c4339a3c6a1920a4250c791b0f00883d775306fb 100644
--- a/why3-coq.opam/opam
+++ b/why3-coq.opam/opam
@@ -24,6 +24,9 @@ tags: [
available: [ ocaml-version >= "4.02.3" ]
build: [
+ ["sh" "-eux" "./run_autoconf_if_needed.sh"] # when used in pinned mode,
+ # the configure *cannot* yet be
+ # generated
["./configure"
"--prefix" prefix
"--disable-why3-lib"
diff --git a/why3-ide.opam/files/run_autoconf_if_needed.sh b/why3-ide.opam/files/run_autoconf_if_needed.sh
new file mode 100644
index 0000000000000000000000000000000000000000..afcace02492ef677436aa93d0fe781e4eea6338a
--- /dev/null
+++ b/why3-ide.opam/files/run_autoconf_if_needed.sh
@@ -0,0 +1,6 @@
+#!/bin/sh -eux
+
+if [ ! -f "configure" ]; then
+ autoconf
+ automake --add-missing || true
+fi
diff --git a/why3-ide.opam/opam b/why3-ide.opam/opam
index d91399d2e824606a88e4e1a8dc38b23eca3050e0..1d02ce3ea95be16689dfbbc77160a8e4e21bed58 100644
--- a/why3-ide.opam/opam
+++ b/why3-ide.opam/opam
@@ -24,6 +24,9 @@ tags: [
available: [ ocaml-version >= "4.02.3" ]
build: [
+ ["sh" "-eux" "./run_autoconf_if_needed.sh"] # when used in pinned mode,
+ # the configure *cannot* yet be
+ # generated
["./configure"
"--prefix" prefix
"--disable-why3-lib"
diff --git a/why3.opam/files/run_autoconf_if_needed.sh b/why3.opam/files/run_autoconf_if_needed.sh
new file mode 100755
index 0000000000000000000000000000000000000000..afcace02492ef677436aa93d0fe781e4eea6338a
--- /dev/null
+++ b/why3.opam/files/run_autoconf_if_needed.sh
@@ -0,0 +1,6 @@
+#!/bin/sh -eux
+
+if [ ! -f "configure" ]; then
+ autoconf
+ automake --add-missing || true
+fi
diff --git a/why3.opam/opam b/why3.opam/opam
index 7de62e0dc92e558fe8cf58279aa8635339961db8..fd0cf31d16a5027ba3606f7bfb9ead37aee39b38 100644
--- a/why3.opam/opam
+++ b/why3.opam/opam
@@ -24,6 +24,9 @@ tags: [
available: [ ocaml-version >= "4.02.3" ]
build: [
+ ["sh" "-eux" "./run_autoconf_if_needed.sh"] # when used in pinned mode,
+ # the configure *cannot* yet be
+ # generated
["./configure"
"--prefix" prefix
"--disable-frama-c"