aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-04-09Fix caching of local hintdb in typeclasses eauto.Matthieu Sozeau
2015-04-08add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.vNickolai Zeldovich
2015-04-08Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)Nickolai Zeldovich
2015-04-07Removing references to -I -as from CHANGES.Pierre-Marie Pédrot
2015-04-06Test for bug #3815.Pierre-Marie Pédrot
2015-04-06refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Nickolai Zeldovich
2015-04-03Use the directory of the current session for selecting files to open.Guillaume Melquiond
2015-04-02Puts all the "import" statements first so as to accommodate the latest GHC.Nickolai Zeldovich
2015-04-02Fix some typos.Guillaume Melquiond
2015-04-02Avoid outputting stray "Local" keywords in HTML documentation.Guillaume Melquiond
2015-04-02Define Any in Haskell extraction when Tunknown is used.Nickolai Zeldovich
2015-04-02Fix compilation of documentation broken by the addition of MMapAVL.Guillaume Melquiond
2015-04-02CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-06 00:58:40 +0000