aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-04-02Make sure that hyperref creates the proper links to the documentation indexes.Guillaume Melquiond
2015-04-02Remove Mltop.add_path as it is no longer possible to import files from subdir...Guillaume Melquiond
2015-04-02Make "Add LoadPath" behave accordingly to its documentation.Guillaume Melquiond
2015-04-02Fix documentation of -R and -Q.Guillaume Melquiond
2015-04-02Make it possible for -R to override the existing implicit setting of a path.Guillaume Melquiond
2015-04-02Display the proper error message when Require fails to find a library.Guillaume Melquiond
2015-04-02MMapAVL: some improved proofs + fix a forgotten AdmittedPierre Letouzey
2015-04-02MMapAVL: implementing MMapInterface via AVL treesPierre Letouzey
2015-04-02ZArith/Int.v: some modernizationsPierre Letouzey
2015-04-02MMapPositive: some improvementsPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:12:05 +0000