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