- 26 Sep, 2011 1 commit
-
-
MARCHE Claude authored
-
- 25 Sep, 2011 1 commit
-
-
Asma Tafat authored
-
- 24 Sep, 2011 3 commits
-
-
Guillaume Melquiond authored
When the user wants to write a Coq proof, she needs to run Coq on the goal, wait five seconds for it to fail (it will fail, otherwise there is no point in running Coq on this goal: another prover would have succeeded already), and finally edit it. This is a waste of time. So goals run with an interactive prover are now marked as unknown until their file is edited. Interactive provers could have been detected by a nonempty "editor" string, but there are interactive provers that don't have dedicated editors, and there might be automated provers with dedicated user interfaces. So a new field was added to prover descriptions. TODO: actually run the editor when there is only one selected goal, rather than keeping the current three-click method of editing proofs.
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 23 Sep, 2011 4 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Asma Tafat authored
-
Asma Tafat authored
-
- 22 Sep, 2011 3 commits
-
-
Guillaume Melquiond authored
t_fold already iters on the subterms of a term, so calling t_fold on a subterm actually iters over grandchildren of the term, which may well be under a quantifier. So t_fold should be called on the term itself. This explains why the transformation was trying to create declarations with unbounded variables.
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
- 21 Sep, 2011 3 commits
-
-
Andrei Paskevich authored
-
Asma Tafat-Bouzid authored
-
Asma Tafat-Bouzid authored
-
- 20 Sep, 2011 19 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
kudos to François for spotting the problem
-
Asma Tafat authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Asma Tafat-Bouzid authored
-
Asma Tafat-Bouzid authored
-
Jean-Christophe Filliâtre authored
-
Asma Tafat-Bouzid authored
-
Asma Tafat-Bouzid authored
-
Asma Tafat-Bouzid authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Asma Tafat-Bouzid authored
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
Guillaume Melquiond authored
fallback on colorizing the identifier.
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 19 Sep, 2011 3 commits
-
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 18 Sep, 2011 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
otherwise we lose the beginning of the transformation chain
-
Andrei Paskevich authored
-