aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-05-07Adding a primitive to the tactic monad to modify the exceptional content.Pierre-Marie Pédrot
2015-05-06Exposing the minimal amount of internal of the Logic monad in order toPierre-Marie Pédrot
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-04Code simplification in Tactics.Pierre-Marie Pédrot
2015-05-04Fix documentation of RedirectEnrico Tassi
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-05-01Fixing computation of implicit arguments by position in fixpoints (#4217).Hugo Herbelin
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo Herbelin
2015-04-28maintenance micromega pluginFrédéric Besson
2015-04-27Improve syntax highlighting.Guillaume Melquiond
2015-04-27Compile the VM code with some optimizations (+130% speedup).Guillaume Melquiond
2015-04-27Fix some ill-typed debugging code in the VM.Guillaume Melquiond
2015-04-26Open the file chooser even if there is no current session. (Fix bug #4206)Guillaume Melquiond
2015-04-25Cleaning some uses of exceptions in tactics.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-23Using tclZEROMSG instead of tclZERO in several places.Pierre-Marie Pédrot
2015-04-23Removing dead code in Pp.Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-22Pp: obsolete comment.Arnaud Spiwack
2015-04-22Declarative mode: remaining goals are "given up" when closing blocks.Arnaud Spiwack
2015-04-22Fixing non exhaustive pattern-matching.Hugo Herbelin
2015-04-22Test for #4198 (appcontext in return clause of match).Hugo Herbelin
2015-04-22More precise numbers about Benjamin's fix for the VM.Maxime Dénès
2015-04-22Update CHANGESMatthieu Sozeau
2015-04-22Do not use list concatenation when gluing streams together, just mark them as...Guillaume Melquiond
2015-04-22Remove some spurious spaces in generated Makefiles.Guillaume Melquiond
2015-04-21STM: print trace on "anomaly, no safe id attached"Enrico Tassi
2015-04-21Fixing #4198 (looking for subterms also in the return clause of match).Hugo Herbelin
2015-04-21Fixing #3383 (a "return" clause without an "in" clause is not enoughHugo Herbelin
2015-04-21Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentHugo Herbelin
2015-04-21Some dead code.Hugo Herbelin
2015-04-20Remove spurious ".v" from warning message.Guillaume Melquiond
2015-04-20Change magic numbers.Matthieu Sozeau
2015-04-20Inlining "fun" and "forall" tokens in parser, so that alternative notations forHugo Herbelin
2015-04-19Slightly more efficient implementation of the logic monad.Pierre-Marie Pédrot
2015-04-178.5beta2 release.Matthieu Sozeau
2015-04-17Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalHugo Herbelin
2015-04-17Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-17No longer add dev/ to the LoadPath, only to the ML path.Guillaume Melquiond
2015-04-16Ensuring purity of datastructures in the API.Pierre-Marie Pédrot
2015-04-16Test for bug #4190.Pierre-Marie Pédrot
2015-04-16Fixing bug #4190.Pierre-Marie Pédrot
2015-04-16configure: fix paths on cygwinEnrico Tassi
2015-04-15Remove dirty debug printing from funind.Maxime Dénès
2015-04-15Documenting the recommandation of toplevel-only commands.Pierre-Marie Pédrot
2015-04-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-14Function now supports puniveresjforest
2015-04-14better debug in recdefjforest
2015-04-14Cleaning up the implementation of search entries in Hints.Pierre-Marie Pédrot
2015-04-14Opaque implementation of auto tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:53:36 +0000