aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Open the file chooser even if there is no current session. (Fix bug #4206)Gravatar Guillaume Melquiond2015-04-26
* Cleaning some uses of exceptions in tactics.Gravatar Pierre-Marie Pédrot2015-04-25
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Removing dead code in Pp.Gravatar Pierre-Marie Pédrot2015-04-23
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Pp: obsolete comment.Gravatar Arnaud Spiwack2015-04-22
* Declarative mode: remaining goals are "given up" when closing blocks.Gravatar Arnaud Spiwack2015-04-22
* Fixing non exhaustive pattern-matching.Gravatar Hugo Herbelin2015-04-22
* Test for #4198 (appcontext in return clause of match).Gravatar Hugo Herbelin2015-04-22
* More precise numbers about Benjamin's fix for the VM.Gravatar Maxime Dénès2015-04-22
* Update CHANGESGravatar Matthieu Sozeau2015-04-22
* Do not use list concatenation when gluing streams together, just mark them as...Gravatar Guillaume Melquiond2015-04-22
* Remove some spurious spaces in generated Makefiles.Gravatar Guillaume Melquiond2015-04-22
* STM: print trace on "anomaly, no safe id attached"Gravatar Enrico Tassi2015-04-21
* Fixing #4198 (looking for subterms also in the return clause of match).Gravatar Hugo Herbelin2015-04-21
* Fixing #3383 (a "return" clause without an "in" clause is not enoughGravatar Hugo Herbelin2015-04-21
* Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentGravatar Hugo Herbelin2015-04-21
* Some dead code.Gravatar Hugo Herbelin2015-04-21
* Remove spurious ".v" from warning message.Gravatar Guillaume Melquiond2015-04-20
* Change magic numbers.Gravatar Matthieu Sozeau2015-04-20
* Inlining "fun" and "forall" tokens in parser, so that alternative notations forGravatar Hugo Herbelin2015-04-20
* Slightly more efficient implementation of the logic monad.Gravatar Pierre-Marie Pédrot2015-04-19
* 8.5beta2 release.Gravatar Matthieu Sozeau2015-04-17
* Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalGravatar Hugo Herbelin2015-04-17
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-17
* No longer add dev/ to the LoadPath, only to the ML path.Gravatar Guillaume Melquiond2015-04-17
* Ensuring purity of datastructures in the API.Gravatar Pierre-Marie Pédrot2015-04-16
* Test for bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* configure: fix paths on cygwinGravatar Enrico Tassi2015-04-16
* Remove dirty debug printing from funind.Gravatar Maxime Dénès2015-04-15
* Documenting the recommandation of toplevel-only commands.Gravatar Pierre-Marie Pédrot2015-04-15
* Function now supports puniveresGravatar jforest2015-04-14
* better debug in recdefGravatar jforest2015-04-14
* Cleaning up the implementation of search entries in Hints.Gravatar Pierre-Marie Pédrot2015-04-14
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
* correction of a bug reported by Tristan CrolardGravatar jforest2015-04-13
* Program: Do not reduce obligation types preemptively, only atGravatar Matthieu Sozeau2015-04-13
* Remove declarations of matched variables in change as an extension ofGravatar Matthieu Sozeau2015-04-13
* More documented representation of hint objects.Gravatar Pierre-Marie Pédrot2015-04-13
* Fixing bug #4186.Gravatar Pierre-Marie Pédrot2015-04-13
* Making the hint entry type opaque.Gravatar Pierre-Marie Pédrot2015-04-12
* Fix compilation broken by Matthieu's last commit.Gravatar Pierre Letouzey2015-04-10
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* Test for bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Eauto hints respect their priority. Fixes bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Making the hints for the auto tactics private.Gravatar Pierre-Marie Pédrot2015-04-10
* Better test-suite files, removing reliance on admit.Gravatar Matthieu Sozeau2015-04-09
* Fix declarations of instances to perform restriction of universeGravatar Matthieu Sozeau2015-04-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:08:39 +0000