coq - The formal proof system

Age	Commit message (Collapse)	Author
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
	This finally closes #5994.
2017-10-28	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin
	This fixes also #5731, #6035, #5364.
2017-10-28	[toplevel] Export the last document seen after `Drop`.	Emilio Jesus Gallego Arias
	After `Drop`, `Coqtop.drop_last_doc` will contain the current document used by `Coqloop`. This is useful for people wanting to restart Coq after a `Drop`.
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
	We are still missing an updated LABLGTK.
2017-10-26	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin
	ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
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
	Fixes #6022.
2017-10-25	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias
	To this extent we factor out the relevant bits to a new file, ltac_pretype.
2017-10-25	Moving from `is_true` to `= true`	Raphaël Monat

2017-10-25	Put linter at the top of the tests.	Théo Zimmermann

2017-10-25	Linter: check that files end with newlines.	Gaëtan Gilbert
	We use git check-attr to look at the same files as git diff --check.
2017-10-25	Put newlines at the end of files.	Gaëtan Gilbert

2017-10-25	Add linter.	Gaëtan Gilbert

2017-10-25	Merge PR #6009: Master+misc typos dead code etc	Maxime Dénès

2017-10-25	Merge PR #6003: Point HoTT back at master, which now supports Coq master	Maxime Dénès

2017-10-25	Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001).	Maxime Dénès

2017-10-25	Merge PR #5995: Revert "Add debug output to brew update."	Maxime Dénès

2017-10-25	Merge PR #5993: Switch testing branch back to CompCert upstream.	Maxime Dénès

2017-10-25	Merge PR #5980: Add AppVeyor badge next to Travis badge.	Maxime Dénès

2017-10-25	Merge PR #5971: [travis] Add flambda testing.	Maxime Dénès

2017-10-24	Fix #5763: Strictly positive example is out of order.	jkloos
	I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example.
2017-10-24	Removing dead code which raised questions.	Hugo Herbelin

2017-10-24	Typo in comment in tactic_matching.ml.	Hugo Herbelin

2017-10-24	An occurrence of set_id which behaves as the identity.	Hugo Herbelin