coq - The formal proof system

Age	Commit message (Expand)	Author
2020-05-03	Further port of the SSR tactics.	Pierre-Marie Pédrot
2020-05-03	Further port of the SSR tactics.	Pierre-Marie Pédrot
2020-05-03	Further port of the SSR tactics.	Pierre-Marie Pédrot
2020-05-03	Further port of the SSR tactics.	Pierre-Marie Pédrot
2020-05-03	Further SSR port.	Pierre-Marie Pédrot
2020-05-03	Remove legacy SSR API.	Pierre-Marie Pédrot
2020-05-03	Further SSR port.	Pierre-Marie Pédrot
2020-05-03	Remove legacy layer in SSR.	Pierre-Marie Pédrot
2020-05-03	Further port of SSR tactics.	Pierre-Marie Pédrot
2020-05-03	Further port of the SSR tactics.	Pierre-Marie Pédrot
2020-05-03	Further port of the SSR code.	Pierre-Marie Pédrot
2020-05-03	Export new combinators in SSR not relying on the legacy API.	Pierre-Marie Pédrot
2020-05-03	Further porting of ssrcode.	Pierre-Marie Pédrot
2020-05-03	Slightly more tricky port of the ssr tactics.	Pierre-Marie Pédrot
2020-05-03	Export missing tacticals.	Pierre-Marie Pédrot
2020-05-03	Further port SSReflect tactics to the new engine.	Pierre-Marie Pédrot
2020-05-03	Wrap ssr tactics into V82.tactic.	Pierre-Marie Pédrot
2020-05-03	Wrap a monadic combinator in a try-with block to catch exceptions.	Pierre-Marie Pédrot
2020-05-03	Remove a call to V82.tactic in Btauto.	Pierre-Marie Pédrot
2020-05-03	Remove a very specific low-level tactical from Refiner.	Pierre-Marie Pédrot
2020-05-03	Wrap Refiner.refiner in the tactic monad.	Pierre-Marie Pédrot
2020-05-03	Remove a critical call to V82.tactic in Clenvtac.	Pierre-Marie Pédrot
2020-05-03	consistency with Permutation	Olivier Laurent
2020-05-03	Simplify division of Cauchy reals	Vincent Semeria
2020-05-03	Ensure eintros allows creating evars	Paolo G. Giarrusso
2020-05-02	Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...	Pierre Roux
2020-05-02	Merge PR #12172: Refactor first chapter: first step, the section on basics.	Clément Pit-Claudel
2020-05-02	Move tclWRAPFINALLY to profile_ltac	Jason Gross
2020-05-02	Decrease LtacProf overhead when not profiling	Jason Gross
2020-05-02	LtacProf now handles multi-success backtracking	Jason Gross
2020-05-02	Add Proofview.tclWRAPFINALLY	Jason Gross
2020-05-02	Adding change logs for PR #12121.	Hugo Herbelin
2020-05-01	Testing different combinations of non truly recursive (co)fixpoints.	Hugo Herbelin
2020-05-01	Changing fixpoint message "decreasing" -> "guarded".	Hugo Herbelin
2020-05-01	Fixing #11903: Fixpoints not truly recursive in standard library.	Hugo Herbelin
2020-05-01	Warn when a (co)fixpoint is not truly recursive.	Hugo Herbelin
2020-05-01	Slight modification of the partial-order algorithm so that it does not	Hugo Herbelin
2020-05-01	Move essential vocabulary and syntax conventions to section on basics.	Théo Zimmermann
2020-05-01	Merge PR #12221: Replace QSeqEquiv by QCauchySeq, simplify proofs.	Michael Soegtrop
2020-05-01	Preserve vernac chapter.	Théo Zimmermann
2020-05-01	Extract two new files out of Gallina chapter.	Théo Zimmermann
2020-05-01	Create section on writing libraries with only deprecated attributes.	Théo Zimmermann
2020-05-01	Extract deprecated attribute from Gallina chapter.	Théo Zimmermann
2020-05-01	Remove flags, options and tables from vernac chapter.	Théo Zimmermann
2020-05-01	Remove lexical conventions and attributes from Gallina chapter.	Théo Zimmermann
2020-05-01	Create basics out of sections from Gallina and Vernac chapters.	Théo Zimmermann
2020-05-01	Create section on basics with just flags, options and tables.	Théo Zimmermann
2020-05-01	Extract flags, options and tables from vernac chapter.	Théo Zimmermann
2020-05-01	Create section on basics with just lexical conventions and attributes.	Théo Zimmermann
2020-05-01	Extract lexical conventions and attributes from Gallina chapter.	Théo Zimmermann