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
*
Status error for bug #3459.
Pierre-Marie Pédrot
2014-09-04
*
Test for bug #3459.
Pierre-Marie Pédrot
2014-09-04
*
Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.
Pierre-Marie Pédrot
2014-09-04
*
Using goal-tactics to interpret arguments to idtac.
Pierre-Marie Pédrot
2014-09-04
*
Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."
Pierre-Marie Pédrot
2014-09-04
*
Revert "Tacinterp: [interp_message] and associate now only require an environ...
Pierre-Marie Pédrot
2014-09-04
*
Revert "Ltac's idtac is now implemented using the new API."
Pierre-Marie Pédrot
2014-09-04
*
Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."
Pierre-Marie Pédrot
2014-09-04
*
Fix bug #3561, correct folding of env in context[] matching.
Matthieu Sozeau
2014-09-04
*
Fix bug #3559, ensuring a canonical order of universe level quantifications when
Matthieu Sozeau
2014-09-04
*
Documenting the [Variant] type definition and the [Nonrecursive Elimination S...
Arnaud Spiwack
2014-09-04
*
Commands like [Inductive > X := … | … | …] raise an error message inste...
Arnaud Spiwack
2014-09-04
*
Factorize the parsing rules of [Record] and the other kind of type definitions.
Arnaud Spiwack
2014-09-04
*
Remove [Infer] option of records.
Arnaud Spiwack
2014-09-04
*
Type definitions with [Variant] don't generate inductive schemes by default.
Arnaud Spiwack
2014-09-04
*
Type definitions [Variant] and [Record] really don't accept the wrong kind of...
Arnaud Spiwack
2014-09-04
*
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
[next]