aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-04-13correction of a bug reported by Tristan Crolardjforest
2015-04-13Program: Do not reduce obligation types preemptively, only atMatthieu Sozeau
2015-04-13Remove declarations of matched variables in change as an extension ofMatthieu Sozeau
2015-04-13More documented representation of hint objects.Pierre-Marie Pédrot
2015-04-13Fixing bug #4186.Pierre-Marie Pédrot
2015-04-12Making the hint entry type opaque.Pierre-Marie Pédrot
2015-04-10Fix compilation broken by Matthieu's last commit.Pierre Letouzey
2015-04-10Fix #3590 for good this time, by changing the API, change's argument nowMatthieu Sozeau
2015-04-10Test for bug #3199.Pierre-Marie Pédrot
2015-04-10Eauto hints respect their priority. Fixes bug #3199.Pierre-Marie Pédrot
2015-04-10Making the hints for the auto tactics private.Pierre-Marie Pédrot
2015-04-09Better test-suite files, removing reliance on admit.Matthieu Sozeau
2015-04-09Fix declarations of instances to perform restriction of universeMatthieu Sozeau
2015-04-09Add test-suite file for bug #4120.Matthieu Sozeau
2015-04-09Really fix constr_of_pattern and bugs #3590 and #4120 byMatthieu Sozeau
2015-04-09Strengthen minimization: it shouldn't set a universe u to a max if itMatthieu Sozeau
2015-04-09Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...Matthieu Sozeau
2015-04-09Prove [map_ext] using [map_ext_in].Nickolai Zeldovich
2015-04-09Add a [map_ext_in] lemma to List.v.Nickolai Zeldovich
2015-04-09JSON extraction: make explicit each group of mutually-recursive fixpointsNickolai Zeldovich
2015-04-09JSON extraction: construct full names (dot-separated) in pp_globalNickolai Zeldovich
2015-04-09Add extraction to JSON.Nickolai Zeldovich
2015-04-09Fix instances of universe-polymorphic generalized rewriting to avoidMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:37:33 +0000