index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Inductive and CoInductive records are printed correctly.
Arnaud Spiwack
2014-09-04
*
Types declared as Variants really do not accept recursive definitions.
Arnaud Spiwack
2014-09-04
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Add a [Variant] declaration which allows to write non-recursive variant types.
Arnaud Spiwack
2014-09-04
*
Add test-suite file for Case derivation on primitive records.
Matthieu Sozeau
2014-09-04
*
Add test suite files for closed bugs.
Matthieu Sozeau
2014-09-04
*
Fix bug #3563, making syntactic matching of primitive projections
Matthieu Sozeau
2014-09-04
*
Putting back normalized goals when entering them.
Pierre-Marie Pédrot
2014-09-03
*
Yes another remaining clearing bug with 'apply in'.
Hugo Herbelin
2014-09-03
*
Fixing printing of unreachable local tactics.
Pierre-Marie Pédrot
2014-09-03
*
Test-suite for bug #2818.
Pierre-Marie Pédrot
2014-09-03
*
Fixing bug #2818.
Pierre-Marie Pédrot
2014-09-03
*
Useless hooks in Tacintern.
Pierre-Marie Pédrot
2014-09-03
*
Code simplification in Tacenv.
Pierre-Marie Pédrot
2014-09-03
*
Print error messages with more hidden information based on α-equivalence .
Arnaud Spiwack
2014-09-03
*
sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex
Pierre Boutillier
2014-09-03
*
Improve RefMan section about Coq_makefile
Pierre Boutillier
2014-09-03
*
Update RefMan with respect to new loadpath management
Pierre Boutillier
2014-09-03
*
Cbn in refman
Pierre Boutillier
2014-09-03
*
Additional entry tactic_arg in Print Grammar tactic.
Pierre-Marie Pédrot
2014-09-03
*
Code factorization in Tacintern.
Pierre-Marie Pédrot
2014-09-03
*
Cleaning code in Pptactic.
Pierre-Marie Pédrot
2014-09-02
*
Adding a test-suite for second-order matching order and indexes.
Pierre-Marie Pédrot
2014-09-02
*
Fixing bug #3136.
Pierre-Marie Pédrot
2014-09-02
*
Another fix than 19a7a5789c to avoid descend_in_conjunction to use
Hugo Herbelin
2014-09-02
*
An apply test.
Hugo Herbelin
2014-09-02
*
Fixup introduction of coqworkmgr
Pierre Boutillier
2014-09-02
*
Removing [revert] tactic from the AST.
Pierre-Marie Pédrot
2014-09-02
*
stm: use xlabel insted of label in dot (debug) output
Enrico Tassi
2014-09-02
*
coqworkmgr
Enrico Tassi
2014-09-02
*
Fix Declaremods.end_library (Closes: #3536)
Enrico Tassi
2014-09-02
*
Removing the 'inductive' parameter from tacexpr AST.
Pierre-Marie Pédrot
2014-09-01
*
Moving the decompose tactic out of the AST.
Pierre-Marie Pédrot
2014-09-01
*
In evarconv, do first-order unification of LetIn's properly, ensuring we comp...
Matthieu Sozeau
2014-09-01
*
Coqide prints succesive hyps of the same type on 1 line
Pierre Boutillier
2014-09-01
*
Code cleaning in Tacintern.
Pierre-Marie Pédrot
2014-09-01
*
Getting rid of atomic tactics in Tacenv.
Pierre-Marie Pédrot
2014-08-31
*
Moving code of tactic interpretation from Tacenv to Vernacentries.
Pierre-Marie Pédrot
2014-08-31
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Type-safe version of genarg list / pair / opt functions.
Pierre-Marie Pédrot
2014-08-29
*
Simplification of Genarg unpackers.
Pierre-Marie Pédrot
2014-08-29
*
Not using a "cut" in descend_in_conjunctions induced more success. We
Hugo Herbelin
2014-08-29
*
Fixing commit 50237af2.
Pierre-Marie Pédrot
2014-08-29
*
Add test-suite file. Compute the name for the record binder in the
Matthieu Sozeau
2014-08-29
*
Fix bug when defining primitive projections mixing defined and abstracts fields.
Matthieu Sozeau
2014-08-29
*
Fixing bug #3528.
Pierre-Marie Pédrot
2014-08-28
*
Simplification of the tclCHECKINTERRUPT tactic.
Pierre-Marie Pédrot
2014-08-28
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
Fix bugs #3484 and #3546.
Matthieu Sozeau
2014-08-28
*
There are some occurs-check cases that can be handled by imitation (using pru...
Matthieu Sozeau
2014-08-28
[next]