coq - The formal proof system

Age	Commit message (Expand)	Author
2017-09-06	changed statements of Rpower_lt and Rle_power and added	Yves Bertot
2017-09-06	Merge PR #1022: Appveyor package	Maxime Dénès
2017-09-05	read flags from project file for Compile Buffer	Paul Steckler
2017-09-05	Refine does not evar-normalizes the goal preemptively.	Pierre-Marie Pédrot
2017-09-05	Make AppVeyor generate Windows package.	Maxime Dénès
2017-09-05	Binding the firstorder tactic.	Pierre-Marie Pédrot
2017-09-05	Remove -debug option from Windows build script.	Maxime Dénès
2017-09-05	Get sources of cygwin packages after building the installer.	Maxime Dénès
2017-09-05	Adapt Windows build script to new CoqIDE data installation directory.	Maxime Dénès
2017-09-05	Print more of the Coq build output.	Maxime Dénès
2017-09-05	Print Coq build output.	Maxime Dénès
2017-09-05	In regression test mode, run cygwin setup to install dependencies.	Maxime Dénès
2017-09-05	Export Ltac2.Notations in the Ltac2 entry module.	Pierre-Marie Pédrot
2017-09-05	The absurd tactic now parses a constr.	Pierre-Marie Pédrot
2017-09-05	Binding move and intro.	Pierre-Marie Pédrot
2017-09-05	Merge PR #1011: fix test-suite/coq-makefile/findlib-package on windows after ...	Maxime Dénès
2017-09-05	Introducing quotations for move locations.	Pierre-Marie Pédrot
2017-09-05	Binding the inversion family of tactics.	Pierre-Marie Pédrot
2017-09-05	Merge PR #1020: .mailmap update	Guillaume Melquiond
2017-09-05	Merge PR #1010: Move mention of native_compute profiling in CHANGES	Maxime Dénès
2017-09-05	Merge PR #1021: Fix Software Foundations build.	Maxime Dénès
2017-09-05	.mailmap update	Gaëtan Gilbert
2017-09-05	Fix Software Foundations build.	Maxime Dénès
2017-09-05	Update CREDITS on a best-effort basis.	Théo Zimmermann
2017-09-05	A few more notations.	Pierre-Marie Pédrot
2017-09-05	Typeclasses_eauto strategy is now optional.	Pierre-Marie Pédrot
2017-09-05	Fixup grammar of typeclasses_eauto.	Pierre-Marie Pédrot
2017-09-05	Quotations for auto-related tactics.	Pierre-Marie Pédrot
2017-09-05	More static invariants for typeclass_eauto.	Pierre-Marie Pédrot
2017-09-05	ML bindings of auto-related tactics.	Pierre-Marie Pédrot
2017-09-04	Notation for "clear - ids".	Pierre-Marie Pédrot
2017-09-04	More notations for primitive tactics.	Pierre-Marie Pédrot
2017-09-04	More precise error messages for scope failure.	Pierre-Marie Pédrot
2017-09-04	Implementing the non-strict mode.	Pierre-Marie Pédrot
2017-09-04	Better backtraces for a few datatypes.	Pierre-Marie Pédrot
2017-09-04	Quick-and-dirty backtrace mechanism for the interpreter.	Pierre-Marie Pédrot
2017-09-04	fix test-suite/coq-makefile/findlib-package on windows	Enrico Tassi
2017-09-04	Merge PR #1018: Avoid reinstalling some Cygwin dependencies on AppVeyor.	Maxime Dénès
2017-09-04	Avoid reinstalling some Cygwin dependencies on AppVeyor.	Maxime Dénès
2017-09-04	Updated gitignore.	Pierre-Marie Pédrot
2017-09-04	Closures now wear the constant they originated from.	Pierre-Marie Pédrot
2017-09-04	Fix coq/ltac2#17: Assertion failed. on only shelved goals remaining.	Pierre-Marie Pédrot
2017-09-04	Implementing multi-match and simple match over constrs.	Pierre-Marie Pédrot
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
2017-09-04	Implementing lazy matching over terms.	Pierre-Marie Pédrot
2017-09-04	Proper anomalies for missing registered primitives.	Pierre-Marie Pédrot
2017-09-03	Introducing a macro for constr matching.	Pierre-Marie Pédrot
2017-09-03	Addressing BZ#5713 (classical_left/classical_right artificially restricted).	Hugo Herbelin
2017-09-03	Moving generic arguments to Tac2quote.	Pierre-Marie Pédrot
2017-09-03	Uniform handling of locations in the various AST.	Pierre-Marie Pédrot