coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-03-21	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
	corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib.
2014-03-26	Adding an interface to Eqdecide and putting the grammar rules in a dedicated	Pierre-Marie Pédrot
	file.