coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-02-17	Ltac as a plugin.	Pierre-Marie Pédrot
	This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
2016-12-07	Merge branch 'v8.6'	Pierre-Marie Pédrot

2016-12-02	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin

2016-11-30	Fix bug #5232: proper globalization of hints paths	Matthieu Sozeau

2016-11-18	Merge branch 'v8.6'	Pierre-Marie Pédrot

2016-11-07	More explicit name for status of unification constraints.	Maxime Dénès

2016-09-21	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot
	There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
2016-09-15	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot

2016-09-14	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot

2016-06-16	Revise syntax of Hint Cut	Matthieu Sozeau
	As noticed by C. Cohen it was confusingly different from standard notation.
2016-06-16	Typeclasses eauto based on new proof engine,	Matthieu Sozeau
	with full backtracking across multiple goals.
2016-04-27	Revert "Fixing printers for pr_auto_using and pr_firstorder_using."	Hugo Herbelin
	This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
2016-04-27	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin

2016-04-12	Removing redundant *_TYPED AS clauses in EXTEND statements.	Pierre-Marie Pédrot

2016-03-25	Moving type_uconstr to Pretyping.	Pierre-Marie Pédrot

2016-03-21	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot