aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Small optimization in Cooking: do not construct identity substitutions.Gravatar Pierre-Marie Pédrot2014-08-13
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* Upgrading output tests.Gravatar Hugo Herbelin2014-08-12
* Bug #3469: fixing unterminated comment.Gravatar Hugo Herbelin2014-08-12
* In bug #2406, renouncing to test failure of parsing error.Gravatar Hugo Herbelin2014-08-12
* Quick fix for avoiding infinitely many respawning and Warning "CoqGravatar Hugo Herbelin2014-08-12
* Fixing parsing of bullets after a "...".Gravatar Hugo Herbelin2014-08-12
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
* Fix bug introduced by earlier commit on first-order unification of primitiveGravatar Matthieu Sozeau2014-08-10
* Fix unification which was failing when unifying a primitive projection againstGravatar Matthieu Sozeau2014-08-09
* Allow pattern matching on the applied form of projections with primitiveGravatar Matthieu Sozeau2014-08-09
* Do early occur-check in unification to allow eta to fire (fixes bug #3477)Gravatar Matthieu Sozeau2014-08-09
* Using the asymmetric merging primitive in Evd.Gravatar Pierre-Marie Pédrot2014-08-09
* Adding a primitive to merge ContextSets which is more efficient when oneGravatar Pierre-Marie Pédrot2014-08-09
* Cleaning up interface of ContextSet.Gravatar Pierre-Marie Pédrot2014-08-09
* Tentative performance fix for Evd.merge_uctx.Gravatar Pierre-Marie Pédrot2014-08-09
* Change internalization of primitive projections to allow parsing [p t] asGravatar Matthieu Sozeau2014-08-08
* Fix evarconv not applying eta when it used to. Fixes bug#3319.Gravatar Matthieu Sozeau2014-08-08
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* More .mailmap update.Gravatar Arnaud Spiwack2014-08-07
* Add some more entries to .mailmapGravatar Arnaud Spiwack2014-08-07
* Hypotheses in [Proofview.Goal.enter] were not normalised.Gravatar Arnaud Spiwack2014-08-07
* In Hipattern: some functions not working modulo evar instantiation.Gravatar Arnaud Spiwack2014-08-07
* Removing simple induction / destruct from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Port last changes of the guard condition to checker.Gravatar Maxime Dénès2014-08-06
* Relax a bit the guard condition.Gravatar Maxime Dénès2014-08-06
* Revert the change in Constrintern introduced by "Add a type of untyped term t...Gravatar Arnaud Spiwack2014-08-06
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
* Adding a [make] primitive to the NonLogical monad.Gravatar Pierre-Marie Pédrot2014-08-05
* Small code simplification.Gravatar Pierre-Marie Pédrot2014-08-05
* CoqIDE: fixing parsing of bullets and brackets even at end of file.Gravatar Hugo Herbelin2014-08-05
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Improving printing of "[]" (nil) in spite of the risk of collisionGravatar Hugo Herbelin2014-08-05
* Preliminary re-installation of notation interpretation in beautifying mode.Gravatar Hugo Herbelin2014-08-05
* Testing beautifying on an example.Gravatar Hugo Herbelin2014-08-05
* Fixing a few beautifying bugs.Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
* Chapter 4 of reference manual: Fixing asymmetric patterns error +Gravatar Hugo Herbelin2014-08-05
* Coqide: check_connection now also checks correct loading of coqide plugin +Gravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* Goal: API to get the solution of a goalGravatar Enrico Tassi2014-08-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 17:10:39 +0000