coq - The formal proof system

Age	Commit message (Expand)	Author
2017-03-03	Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.	Hugo Herbelin
2017-03-03	Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.	Hugo Herbelin
2017-03-03	Completing "few lemmas about Zneg" with lemmas also about Zpos.	Hugo Herbelin
2017-03-03	A couple of other useful properties about compare_cont.	Hugo Herbelin
2017-03-03	Compatibility of iff wrt not and imp.	Hugo Herbelin
2017-03-03	Formatting references with surrounding brackets in Diaconescu.v.	Hugo Herbelin
2017-03-03	[ltac] Move dummy plugin to plugins folder.	Emilio Jesus Gallego Arias
2017-03-02	[travis] Backport trunk's travis support.	Emilio Jesus Gallego Arias
2017-03-01	Add η principles for sigma types	Jason Gross
2017-03-01	Remove some trailing whitespace in Init/Specif.v	Jason Gross
2017-02-27	Merge PR#399: Debug by default	Maxime Dénès
2017-02-27	Merge PR#395: Allow hintdb to be parameters in a Ltac definition or	Maxime Dénès
2017-02-27	Do not recompute twice the whnf of terms in conversion.	Pierre-Marie Pédrot
2017-02-24	[travis] [External CI] fiat-parsers	Emilio Jesus Gallego Arias
2017-02-24	TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès
2017-02-24	Revert "Add empty ltac_plugin file for forward compatibility."	Maxime Dénès
2017-02-24	Simplifying the proof of NoRetractToModalProposition.paradox in	Hugo Herbelin
2017-02-24	Fixing anomaly on unsupported key in interactive ltac debug.	Hugo Herbelin
2017-02-23	Fixing a little bug in printing ex2 (type was printed "_" by default).	Hugo Herbelin
2017-02-23	Fixing a little bug in using the "where" clause for inductive types.	Hugo Herbelin
2017-02-23	Fixing #use"include" after vernac is added and ltac is moved to a plugin.	Hugo Herbelin
2017-02-22	Merge branch 'v8.6'	Pierre-Marie Pédrot
2017-02-22	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot
2017-02-21	Allow interactive editing of Coq.Init.Logic	Jason Gross
2017-02-21	[travis] track an 8.7 specific branch of HoTT.	Maxime Dénès
2017-02-21	Merge PR#309: Ltac as a plugin	Maxime Dénès
2017-02-21	Add empty ltac_plugin file for forward compatibility.	Maxime Dénès
2017-02-20	Fix V7 syntax in refman.	Théo Zimmermann
2017-02-20	Deprecate -debug flag.	Maxime Dénès
2017-02-20	Merge PR#189: Remove tabulation support from pretty-printing.	Maxime Dénès
2017-02-20	Merge pull request #4 from Zimmi48/patch-1	Emilio Jesús Gallego Arias
2017-02-20	[ocamlbuild] fix small mistakes in descriptions	Théo Zimmermann
2017-02-20	[ocamlbuild] Update meta for the vernac split.	Emilio Jesus Gallego Arias
2017-02-19	Fixing debugger after the split of toplevel into vernac.	Pierre-Marie Pédrot
2017-02-19	Optimizing array mapping in the kernel.	Pierre-Marie Pédrot
2017-02-17	remove obsolete file dev/Makefile.oug	Pierre Letouzey
2017-02-17	Removing spurious folder includes in coq_makefile.	Pierre-Marie Pédrot
2017-02-17	Documenting the pluginification of Ltac.	Pierre-Marie Pédrot
2017-02-17	Fix .gitignore.	Pierre-Marie Pédrot
2017-02-17	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot
2017-02-17	Ltac as a plugin.	Pierre-Marie Pédrot
2017-02-16	Fixing #5339 (anomaly with 'pat in record parameters).	Hugo Herbelin
2017-02-16	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed
2017-02-16	reject notations that are both 'only printing' and 'only parsing'	Ralf Jung
2017-02-16	don't require printing-only notation to be productive	Ralf Jung
2017-02-16	Merge PR#403: Split Vernacular Processing from Toplevel	Maxime Dénès
2017-02-16	Merge PR#431	Maxime Dénès
2017-02-15	[travis] [External CI] CompCert official 8.6 support + UniMath	Emilio Jesus Gallego Arias
2017-02-15	[travis] [External CI] Factor out math-comp installs.	Emilio Jesus Gallego Arias
2017-02-15	Make Obligations see fix_exn	Enrico Tassi