coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-04-10	Do not compute constr matching context if not used.	Pierre-Marie Pédrot
	This mitigates bug #6860.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-12-11	Remove deprecated option Tactic Compat Context.	Théo Zimmermann
	And some code simplification.
2017-12-09	Remove up-to-conversion matching functions.	Pierre-Marie Pédrot
	They were not used anymore since the previous patches.
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
	We do up to `Term` which is the main bulk of the changes.
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-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-02-14	Tactic_matching API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Constr_matching API using EConstr.	Pierre-Marie Pédrot

2016-09-08	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot

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

2015-10-11	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin
	Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables.
2015-01-12	Update headers.	Maxime Dénès

2015-01-08	Avoiding introducing yet another convention in naming files.	Hugo Herbelin