- 15 Dec, 2011 2 commits
-
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
- 14 Dec, 2011 4 commits
-
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Guillaume Melquiond authored
-
- 13 Dec, 2011 1 commit
-
-
Andrei Paskevich authored
-
- 08 Dec, 2011 2 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 06 Dec, 2011 3 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 01 Dec, 2011 5 commits
-
-
Guillaume Melquiond authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
- 30 Nov, 2011 10 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
ntmtuyen authored
-
ntmtuyen authored
-
Thi-Minh-Tuyen Nguyen authored
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
François Bobot authored
- When the encoding can't encode a definition it transform it into an axiom. But it's not the same than before. The differences is that eliminate algebraic is before this transformation into axiom and not after. So if the definition start with a match, in one case that give different nice axioms, and in the other case that introduce a match function which is polymorph and not well used by provers. Possible solutions : 1) make the match function easier to use with some modification to its definition and discriminate it. 2) Eliminate the match function when the encoding tranform a definition into axioms. This reverts commit 1f652980.
-
- 29 Nov, 2011 2 commits
-
-
Guillaume Melquiond authored
-
Thi-Minh-Tuyen Nguyen authored
-
- 28 Nov, 2011 1 commit
-
-
Andrei Paskevich authored
-
- 27 Nov, 2011 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 26 Nov, 2011 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 24 Nov, 2011 2 commits
-
-
Guillaume Melquiond authored
Moreover, - Coq realizations are disabled for Coq < 8.3 due to coqdep bugs, - Whyconf.magicnumber is incremented to ensure coqc and coqide are called with -R, - realizations for FP arithmetic are disabled if Flocq is missing.
-
Guillaume Melquiond authored
-
- 23 Nov, 2011 3 commits
-
-
-
MARCHE Claude authored
-
Thi-Minh-Tuyen Nguyen authored
-
- 20 Nov, 2011 2 commits
-
-
Guillaume Melquiond authored
Note that this is just a consequence of symbols not being imported from realizations. If Coq files were generated with "Require Import" directives rather than just "Require", the change would have been completely transparent. This is not reason enough to switch to "Require Import" but it should be kept in mind.
-
Guillaume Melquiond authored
My first idea was to use "-R @libdir@/coq", or some other variable I would have defined in configure.in, but it didn't work at all. Indeed, such path variables depend on cascaded substitution, which work fine inside make files and shell scripts, but not at all inside Why3 config files. Note that this is a documented feature of Autoconf so I doubt there is any way to circumvent it. So I ended up adding a new format specifier inside call_provers: %l is substituted by Config.libdir.
-