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-06-16	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin
	simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-05-16	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot

2016-05-08	Removing dead code and unused opens.	Pierre-Marie Pédrot

2016-05-04	Do not generate generic arguments for data which only requires toplevel values.	Pierre-Marie Pédrot

2016-05-04	Moving the Val module to Geninterp.	Pierre-Marie Pédrot

2016-05-04	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot

2016-04-27	Revert "In the short term, stronger invariant on the syntax of TacAssert, what"	Hugo Herbelin
	This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
2016-04-27	In the short term, stronger invariant on the syntax of TacAssert, what	Hugo Herbelin
	allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-03-21	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot