aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Function now supports puniveresGravatar jforest2015-04-14
* better debug in recdefGravatar jforest2015-04-14
* Cleaning up the implementation of search entries in Hints.Gravatar Pierre-Marie Pédrot2015-04-14
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
* correction of a bug reported by Tristan CrolardGravatar jforest2015-04-13
* Program: Do not reduce obligation types preemptively, only atGravatar Matthieu Sozeau2015-04-13
* Remove declarations of matched variables in change as an extension ofGravatar Matthieu Sozeau2015-04-13
* More documented representation of hint objects.Gravatar Pierre-Marie Pédrot2015-04-13
* Fixing bug #4186.Gravatar Pierre-Marie Pédrot2015-04-13
* Making the hint entry type opaque.Gravatar Pierre-Marie Pédrot2015-04-12
* Fix compilation broken by Matthieu's last commit.Gravatar Pierre Letouzey2015-04-10
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* Test for bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Eauto hints respect their priority. Fixes bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Making the hints for the auto tactics private.Gravatar Pierre-Marie Pédrot2015-04-10
* Better test-suite files, removing reliance on admit.Gravatar Matthieu Sozeau2015-04-09
* Fix declarations of instances to perform restriction of universeGravatar Matthieu Sozeau2015-04-09
* Add test-suite file for bug #4120.Gravatar Matthieu Sozeau2015-04-09
* Really fix constr_of_pattern and bugs #3590 and #4120 byGravatar Matthieu Sozeau2015-04-09
* Strengthen minimization: it shouldn't set a universe u to a max if itGravatar Matthieu Sozeau2015-04-09
* Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...Gravatar Matthieu Sozeau2015-04-09
* Prove [map_ext] using [map_ext_in].Gravatar Nickolai Zeldovich2015-04-09
* Add a [map_ext_in] lemma to List.v.Gravatar Nickolai Zeldovich2015-04-09
* JSON extraction: make explicit each group of mutually-recursive fixpointsGravatar Nickolai Zeldovich2015-04-09
* JSON extraction: construct full names (dot-separated) in pp_globalGravatar Nickolai Zeldovich2015-04-09
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
* Fix instances of universe-polymorphic generalized rewriting to avoidGravatar Matthieu Sozeau2015-04-09
* Fix caching of local hintdb in typeclasses eauto.Gravatar Matthieu Sozeau2015-04-09
* add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.vGravatar Nickolai Zeldovich2015-04-08
* Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)Gravatar Nickolai Zeldovich2015-04-08
* Removing references to -I -as from CHANGES.Gravatar Pierre-Marie Pédrot2015-04-07
* Test for bug #3815.Gravatar Pierre-Marie Pédrot2015-04-06
* refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Gravatar Nickolai Zeldovich2015-04-06
* Use the directory of the current session for selecting files to open.Gravatar Guillaume Melquiond2015-04-03
* Puts all the "import" statements first so as to accommodate the latest GHC.Gravatar Nickolai Zeldovich2015-04-02
* Fix some typos.Gravatar Guillaume Melquiond2015-04-02
* Avoid outputting stray "Local" keywords in HTML documentation.Gravatar Guillaume Melquiond2015-04-02
* Define Any in Haskell extraction when Tunknown is used.Gravatar Nickolai Zeldovich2015-04-02
* Fix compilation of documentation broken by the addition of MMapAVL.Gravatar Guillaume Melquiond2015-04-02
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
* Make sure that hyperref creates the proper links to the documentation indexes.Gravatar Guillaume Melquiond2015-04-02
* Remove Mltop.add_path as it is no longer possible to import files from subdir...Gravatar Guillaume Melquiond2015-04-02
* Make "Add LoadPath" behave accordingly to its documentation.Gravatar Guillaume Melquiond2015-04-02
* Fix documentation of -R and -Q.Gravatar Guillaume Melquiond2015-04-02
* Make it possible for -R to override the existing implicit setting of a path.Gravatar Guillaume Melquiond2015-04-02
* Display the proper error message when Require fails to find a library.Gravatar Guillaume Melquiond2015-04-02
* MMapAVL: some improved proofs + fix a forgotten AdmittedGravatar Pierre Letouzey2015-04-02
* MMapAVL: implementing MMapInterface via AVL treesGravatar Pierre Letouzey2015-04-02
* ZArith/Int.v: some modernizationsGravatar Pierre Letouzey2015-04-02
* MMapPositive: some improvementsGravatar Pierre Letouzey2015-04-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 02:50:13 +0000