aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-05-05Compatibility ocaml 3.12.Hugo Herbelin
2015-05-05Granting wish #4221.Pierre-Marie Pédrot
2015-05-05Fix bug #4212, congruence forgetting about some universe constraints.Matthieu Sozeau
2015-05-05Removing dead code in Rewrite.Pierre-Marie Pédrot
2015-05-05Making the strategy type in Rewrite opaque.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-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-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 12:11:52 +0000