aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-01
* More clarifications on loadpaths.Gravatar Pierre-Marie Pédrot2015-04-01
* Documenting "From * Require *" and clearing a bit the loadpath chapter.Gravatar Pierre-Marie Pédrot2015-04-01
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing inclusion of user contrib directory in the loadpath.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* Removing the unused root flag from loadpaths.Gravatar Pierre-Marie Pédrot2015-03-31
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-03-31
* A more reasonable implementation of Loadpath.Gravatar Pierre-Marie Pédrot2015-03-31
* Declarative mode: fix proof modes.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: fix vernac classification.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: plug the specialised printers back.Gravatar Arnaud Spiwack2015-03-31
* Better formatting of messages in proofs.Gravatar Arnaud Spiwack2015-03-31
* Generalisation of the "end command" argument of the goal printer.Gravatar Arnaud Spiwack2015-03-31
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-06 16:23:15 +0000