coq - The formal proof system

Age	Commit message (Expand)	Author
2015-04-09	Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...	Matthieu Sozeau
2015-04-09	Prove [map_ext] using [map_ext_in].	Nickolai Zeldovich
2015-04-09	Add a [map_ext_in] lemma to List.v.	Nickolai Zeldovich
2015-04-09	JSON extraction: make explicit each group of mutually-recursive fixpoints	Nickolai Zeldovich
2015-04-09	JSON extraction: construct full names (dot-separated) in pp_global	Nickolai Zeldovich
2015-04-09	Add extraction to JSON.	Nickolai Zeldovich
2015-04-09	Fix instances of universe-polymorphic generalized rewriting to avoid	Matthieu Sozeau
2015-04-09	Fix caching of local hintdb in typeclasses eauto.	Matthieu Sozeau
2015-04-08	add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.v	Nickolai Zeldovich
2015-04-08	Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)	Nickolai Zeldovich
2015-04-07	Removing references to -I -as from CHANGES.	Pierre-Marie Pédrot
2015-04-06	Test for bug #3815.	Pierre-Marie Pédrot
2015-04-06	refresh metas in rewrite hints loaded from .vo files (fix bug #3815)	Nickolai Zeldovich
2015-04-03	Use the directory of the current session for selecting files to open.	Guillaume Melquiond
2015-04-02	Puts all the "import" statements first so as to accommodate the latest GHC.	Nickolai Zeldovich
2015-04-02	Fix some typos.	Guillaume Melquiond
2015-04-02	Avoid outputting stray "Local" keywords in HTML documentation.	Guillaume Melquiond
2015-04-02	Define Any in Haskell extraction when Tunknown is used.	Nickolai Zeldovich
2015-04-02	Fix compilation of documentation broken by the addition of MMapAVL.	Guillaume Melquiond
2015-04-02	CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)	Enrico Tassi
2015-04-02	Make sure that hyperref creates the proper links to the documentation indexes.	Guillaume Melquiond
2015-04-02	Remove Mltop.add_path as it is no longer possible to import files from subdir...	Guillaume Melquiond
2015-04-02	Make "Add LoadPath" behave accordingly to its documentation.	Guillaume Melquiond
2015-04-02	Fix documentation of -R and -Q.	Guillaume Melquiond
2015-04-02	Make it possible for -R to override the existing implicit setting of a path.	Guillaume Melquiond
2015-04-02	Display the proper error message when Require fails to find a library.	Guillaume Melquiond
2015-04-02	MMapAVL: some improved proofs + fix a forgotten Admitted	Pierre Letouzey
2015-04-02	MMapAVL: implementing MMapInterface via AVL trees	Pierre Letouzey
2015-04-02	ZArith/Int.v: some modernizations	Pierre Letouzey
2015-04-02	MMapPositive: some improvements	Pierre Letouzey
2015-04-01	Accomodating #4166 (providing "Require Import OmegaTactic" as a	Hugo Herbelin
2015-04-01	Fixing a few typos + some uniformization of writing in doc.	Hugo Herbelin
2015-04-01	More clarifications on loadpaths.	Pierre-Marie Pédrot
2015-04-01	Documenting "From * Require *" and clearing a bit the loadpath chapter.	Pierre-Marie Pédrot
2015-04-01	From X Require Y looks for X with absolute path, disregarding -R.	Pierre-Marie Pédrot
2015-04-01	Fixing inclusion of user contrib directory in the loadpath.	Pierre-Marie Pédrot
2015-04-01	Fixing test-suite.	Pierre-Marie Pédrot
2015-04-01	Removing a probably incorrect on-the-fly require in a tactic.	Pierre-Marie Pédrot
2015-03-31	Removing references to deprecated syntax -I/-R -as.	Pierre-Marie Pédrot
2015-03-31	Removing the unused root flag from loadpaths.	Pierre-Marie Pédrot
2015-03-31	Fixing test-suite.	Pierre-Marie Pédrot
2015-03-31	A more reasonable implementation of Loadpath.	Pierre-Marie Pédrot
2015-03-31	Declarative mode: fix proof modes.	Arnaud Spiwack
2015-03-31	Declarative mode: fix vernac classification.	Arnaud Spiwack
2015-03-31	Declarative mode: plug the specialised printers back.	Arnaud Spiwack
2015-03-31	Better formatting of messages in proofs.	Arnaud Spiwack
2015-03-31	Generalisation of the "end command" argument of the goal printer.	Arnaud Spiwack
2015-03-31	Fix various typos in documentation	Matěj Grabovský
2015-03-31	Do not escape "'" when outputting to html, especially not using "´".	Guillaume Melquiond
2015-03-30	grammar: export constr_eval	Enrico Tassi