coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-15	Search: new clauses for searching head, conclusion, kind...	Hugo Herbelin
	- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict match to an hypothesis or the conclusion, possibly only at the head (like SearchHead in this latter case) - new clause "is:" to search by kind of object (for some list of kinds) - support for any combination of negations, disjunctions and conjunctions, using a syntax close to that of intropatterns.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-10-30	[declare] Remove declare_scheme hook in Declare	Emilio Jesus Gallego Arias
	We introduce a new module that registers the scheme information that side-effects need, thus removing the hook from `Declare`. As we may want to deprecate scheme side effects, there is no need to design a general mechanism for this kind of registration for now. Would we remove the scheme side-effects the scheme code could become self-contained again.