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
*
Fix test-suite file.
Matthieu Sozeau
2014-08-18
*
Fix test-suite files.
Matthieu Sozeau
2014-08-18
*
Refine patch for behavior of unify_to_subterm to allow backtracking on
Matthieu Sozeau
2014-08-18
*
Fix test-suite file.
Matthieu Sozeau
2014-08-18
*
Fixing include of debugger.
Pierre-Marie Pédrot
2014-08-18
*
Moving the TacAlias node out of atomic tactics.
Pierre-Marie Pédrot
2014-08-18
*
Moving the TacExtend node from atomic to plain tactics.
Pierre-Marie Pédrot
2014-08-18
*
Removing documentation related to the deprecated State machinery.
Pierre-Marie Pédrot
2014-08-16
*
Better printing of Ltac values.
Pierre-Marie Pédrot
2014-08-16
*
Fixing too restrictive detection of resolution of evars in "apply in"
Hugo Herbelin
2014-08-16
*
More self-contained code for tclWITHHOLES.
Pierre-Marie Pédrot
2014-08-15
*
Removing unused Refiner.tclWITHHOLES.
Pierre-Marie Pédrot
2014-08-15
*
Remove confusing behavior of unify_with_subterm that could fail with
Matthieu Sozeau
2014-08-14
*
Fix program using an the unsubstituted type of the original obligation
Matthieu Sozeau
2014-08-14
*
Fix non-printing of coercions for primitive projections (fixes bug #3433).
Matthieu Sozeau
2014-08-14
*
Restrict eta-conversion to inductive records, fixing bug #3310.
Matthieu Sozeau
2014-08-14
*
Restore the error-handling behavior of [change], which was silently failing
Matthieu Sozeau
2014-08-14
*
Fix elimschemes accessing directly the universe context of inductives (fixes ...
Matthieu Sozeau
2014-08-14
*
Fix test-suite files according to new parsing rule for application of primitive
Matthieu Sozeau
2014-08-13
*
Small optimization in Cooking: do not construct identity substitutions.
Pierre-Marie Pédrot
2014-08-13
*
Bettre pretty-printing of evar maps, avoids printing universe information
Matthieu Sozeau
2014-08-13
*
Upgrading output tests.
Hugo Herbelin
2014-08-12
*
Bug #3469: fixing unterminated comment.
Hugo Herbelin
2014-08-12
*
In bug #2406, renouncing to test failure of parsing error.
Hugo Herbelin
2014-08-12
*
Quick fix for avoiding infinitely many respawning and Warning "Coq
Hugo Herbelin
2014-08-12
*
Fixing parsing of bullets after a "...".
Hugo Herbelin
2014-08-12
*
A couple of fixes/improvements in -beautify, but backtracking on
Hugo Herbelin
2014-08-12
*
Fix bug introduced by earlier commit on first-order unification of primitive
Matthieu Sozeau
2014-08-10
*
Fix unification which was failing when unifying a primitive projection against
Matthieu Sozeau
2014-08-09
*
Allow pattern matching on the applied form of projections with primitive
Matthieu Sozeau
2014-08-09
*
Do early occur-check in unification to allow eta to fire (fixes bug #3477)
Matthieu Sozeau
2014-08-09
*
Using the asymmetric merging primitive in Evd.
Pierre-Marie Pédrot
2014-08-09
*
Adding a primitive to merge ContextSets which is more efficient when one
Pierre-Marie Pédrot
2014-08-09
*
Cleaning up interface of ContextSet.
Pierre-Marie Pédrot
2014-08-09
*
Tentative performance fix for Evd.merge_uctx.
Pierre-Marie Pédrot
2014-08-09
*
Change internalization of primitive projections to allow parsing [p t] as
Matthieu Sozeau
2014-08-08
*
Fix evarconv not applying eta when it used to. Fixes bug#3319.
Matthieu Sozeau
2014-08-08
*
Better structure for Ltac pretyping environments.
Pierre-Marie Pédrot
2014-08-07
*
More .mailmap update.
Arnaud Spiwack
2014-08-07
*
Add some more entries to .mailmap
Arnaud Spiwack
2014-08-07
*
Hypotheses in [Proofview.Goal.enter] were not normalised.
Arnaud Spiwack
2014-08-07
*
In Hipattern: some functions not working modulo evar instantiation.
Arnaud Spiwack
2014-08-07
*
Removing simple induction / destruct from the AST.
Pierre-Marie Pédrot
2014-08-07
*
Instead of relying on a trick to make the constructor tactic parse, put
Pierre-Marie Pédrot
2014-08-07
*
Removing the "constructor" tactic from the AST.
Pierre-Marie Pédrot
2014-08-07
*
Port last changes of the guard condition to checker.
Maxime Dénès
2014-08-06
*
Relax a bit the guard condition.
Maxime Dénès
2014-08-06
*
Revert the change in Constrintern introduced by "Add a type of untyped term t...
Arnaud Spiwack
2014-08-06
*
[uconstr]: use a closure instead of eager substitution.
Arnaud Spiwack
2014-08-06
*
Removing "intros untils" from the AST.
Pierre-Marie Pédrot
2014-08-06
[next]