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 unblocking code in dependent destruction due to zeta being used in unfold...
msozeau
2012-02-01
*
Corrected a careless cut-and-paste in Gallina description which dated back to...
ppedrot
2012-02-01
*
Debugger vs tracer: Two different behaviors wrt printing: The debugger
herbelin
2012-02-01
*
Improved synchronisation of stdlib index page with current library state.
herbelin
2012-02-01
*
Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...
msozeau
2012-01-31
*
index-list.html.template: add missing files
pboutill
2012-01-31
*
Fix consequence of pp bugfix in testsuite
pboutill
2012-01-31
*
Makefile.build: add targets install-devfiles and install-ide-devfiles
pboutill
2012-01-31
*
Bug #2041: unfold at betaiotaZETA normalize like unfold
pboutill
2012-01-31
*
Fix camlp4 compilation
pboutill
2012-01-31
*
Added an pattern / occurence syntax for vm_compute.
ppedrot
2012-01-30
*
Tentative to fix bug #2628 by not letting intuition break records. Might be t...
msozeau
2012-01-28
*
Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...
msozeau
2012-01-28
*
Printing bugs with match patterns:
herbelin
2012-01-27
*
Fail: discard the effects of a successful command (fix #2682)
letouzey
2012-01-26
*
Add support for plugin initialization function
gareuselesinge
2012-01-26
*
Check for unresolved evars in textual order of the params and fields declarat...
msozeau
2012-01-25
*
Fix bug #2483: anomaly raised due to wrong handling of the evars state.
msozeau
2012-01-23
*
Fix typeclass resolution error message which included goal evars (bug #2620).
msozeau
2012-01-23
*
Fix for Program Instance not separately checking the resolution of evars of t...
msozeau
2012-01-23
*
Another quick hack that works this time, to handle printing of locality in Pr...
ppedrot
2012-01-23
*
Deleted the only use of BeginSubProof from the standard library.
ppedrot
2012-01-23
*
Removed a seemingly unused argument in Require of modules, introduced 10 year...
ppedrot
2012-01-23
*
Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.
ppedrot
2012-01-23
*
Bug 739: forbid dumpglob while using Coqtop in interactive mode
pboutill
2012-01-23
*
Coqtop and coqc: cleaning description of options in RefMan and manpages.
pboutill
2012-01-21
*
Added documentation for "r foo" in Ltac debugger.
herbelin
2012-01-20
*
Added documentation for "Set Parsing Explicit" + fixed mistakenly
herbelin
2012-01-20
*
Breakpoints in Ltac debugger: new command "r foo" to jump to the next
herbelin
2012-01-20
*
Added new command "Set Parsing Explicit" for deactivating parsing (and
herbelin
2012-01-20
*
Notations with binders: Accepting using notations for functional terms
herbelin
2012-01-20
*
Reverted previous commit, which broke library compilation.
ppedrot
2012-01-20
*
This is a quick hack to permit the parsing of the locality flag in the Progra...
ppedrot
2012-01-20
*
Fix printing of classes
msozeau
2012-01-20
*
Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.
msozeau
2012-01-19
*
Added the btauto tactic to the documentation.
ppedrot
2012-01-19
*
Pretty printing of generalized binder
pboutill
2012-01-19
*
Boolean Option Patterns Compatibility
pboutill
2012-01-19
*
No more use of tauto in Init/
pboutill
2012-01-19
*
Fixed the pretty-printing of the Program plugin.
ppedrot
2012-01-17
*
Makefile: fix make distclean w.r.t. test-suite
letouzey
2012-01-17
*
MSetAVL: better implementation of filter suggested by X. Leroy
letouzey
2012-01-17
*
Some fix in beautify pretty-printer
pboutill
2012-01-17
*
Parameters in pattern first step.
pboutill
2012-01-16
*
Inductiveops.nb_*{,_env} cleaning
pboutill
2012-01-16
*
Bug 2679: Do not try to install cmxs with -byte-only
pboutill
2012-01-16
*
Bug 2676: ./configure --prefix shoudn't ask for a config directory.
pboutill
2012-01-16
*
make mli-doc fix
pboutill
2012-01-16
*
coq_micromega.ml: fix order of recursive calls to rconstant
glondu
2012-01-14
*
Add distclean back to test-suite/Makefile
glondu
2012-01-14
[prev]
[next]