coq - The formal proof system

Age	Commit message (Expand)	Author
2017-11-02	Binding the specialize tactic.	Pierre-Marie Pédrot
2017-11-02	Ltac Debug: exporting env and sigma when needed so that term can be printed.	Hugo Herbelin
2017-11-02	Binding ltac printing functions to the system of generic printing.	Hugo Herbelin
2017-11-02	Setting a system to register printers for Ltac values.	Hugo Herbelin
2017-11-02	Exporting ValTMap for use in Genintern.	Hugo Herbelin
2017-11-02	Using a specific function to register vernac printers.	Hugo Herbelin
2017-11-02	Exporting the level-parametric printer of constr and its variants.	Hugo Herbelin
2017-11-02	Do not identify a pre_ident as a string Ltac value.	Hugo Herbelin
2017-11-02	Removing a redundancy in naming types (Ppconstr.precedence = tolerability).	Hugo Herbelin
2017-11-02	Naming the type of Dyn.Map for future reuse.	Hugo Herbelin
2017-11-02	Exporting a few more printing functions.	Hugo Herbelin
2017-11-02	Improving checks about the list separator in tactic notations.	Hugo Herbelin
2017-11-01	[API] Some reordering following latest separation commits.	Emilio Jesus Gallego Arias
2017-11-01	[general] Move Tactypes to `interp`	Emilio Jesus Gallego Arias
2017-11-01	Fix FIXME: use OCaml 4.02 generative functors when available.	Gaëtan Gilbert
2017-11-01	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík
2017-10-30	Fixing #2881 ("change with" failing in an Ltac definition).	Hugo Herbelin
2017-10-30	Add a macro for the now tactic	Pierre-Marie Pédrot
2017-10-30	Put notations in level 5 by default.	Pierre-Marie Pédrot
2017-10-30	Fix the semantics of introducing with empty intro patterns.	Pierre-Marie Pédrot
2017-10-30	Introducing the change tactic.	Pierre-Marie Pédrot
2017-10-30	Fix compilation after merge of Ltac_pretype interface.	Pierre-Marie Pédrot
2017-10-30	[ci] Switch VST back to upstream.	Théo Zimmermann
2017-10-28	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin
2017-10-28	[toplevel] Export the last document seen after `Drop`.	Emilio Jesus Gallego Arias
2017-10-27	[ci] Switch back to upstream version of Math-Classes and Corn.	Théo Zimmermann
2017-10-27	Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.	Théo Zimmermann
2017-10-27	Adding documentation	Pierre-Marie Pédrot
2017-10-27	Better printers for toplevel values.	Pierre-Marie Pédrot
2017-10-27	Adding an OPAM package.	Pierre-Marie Pédrot
2017-10-27	Adding a notation for match goal.	Pierre-Marie Pédrot
2017-10-27	Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing.	Maxime Dénès
2017-10-27	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès
2017-10-27	Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631	Maxime Dénès
2017-10-27	Merge PR #5979: Fix #5763: Strictly positive example is out of order.	Maxime Dénès
2017-10-27	Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful	Maxime Dénès
2017-10-27	Merge PR #677: Trunk+abstracting injection flags	Maxime Dénès
2017-10-27	Adding a command to evaluate Ltac2 expressions.	Pierre-Marie Pédrot
2017-10-27	Fix goal_matching quotation.	Pierre-Marie Pédrot
2017-10-27	Fix relative meaning of Pattern vs. Context in match goal.	Pierre-Marie Pédrot
2017-10-27	Stubs for goal matching: quotation and matching function.	Pierre-Marie Pédrot
2017-10-27	Chaining two tactics in a proof	Raphaël Monat
2017-10-27	[ocaml] [travis] Add preliminary 4.06 CI testing.	Emilio Jesus Gallego Arias
2017-10-26	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin
2017-10-26	Delay use of flag "Discriminate Introduction" from interp to execution time.	Hugo Herbelin
2017-10-26	Updating version history wrt 8.7.	Hugo Herbelin
2017-10-26	Updating version history wrt 8.6.	Hugo Herbelin
2017-10-26	Updating version history wrt 8.5.	Hugo Herbelin
2017-10-25	Rename \Tree to \NatTree	Johannes Kloos
2017-10-25	Use GHC.Base.Any for compatibility with GHC 8.2	Tej Chajed