coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Using appropriate lambda decomposition function counting let-ins when	Hugo Herbelin	2015-10-18
\| \| \| \| \| \| \| \|	dealing with "match". Contrastingly, "fix" is considered not to count let-ins for finding the recursive argument (which is ok because the last argument is necessarily a lambda).
*	Fix constr_matching when a match is found in the head of a case construct	Matthieu Sozeau	2015-10-14
\|
*	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
\| \| \| \| \| \|	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.
*	Constr_matching: renaming misleading name stk into ctx.	Hugo Herbelin	2015-10-11
\|
*	Better fixing #4198 such that the term to match is looked for before	Hugo Herbelin	2015-05-13
\| \| \| \| \| \| \|	the predicate, thus respecting the visual left-to-right top-down order (see a45bd5981092). This fixes CFGV.
*	Code factorization in Constr_matching.	Pierre-Marie Pédrot	2015-05-10
\|
*	Fixing #4198 (looking for subterms also in the return clause of match).	Hugo Herbelin	2015-04-21
\| \| \| \| \|	This is actually not so perfect because of the lambdas in the return clause which we would not like to look in.
*	Ensuring more invariants in Constr_matching.	Pierre-Marie Pédrot	2015-03-29
\|
*	Fixing bug #4165.	Pierre-Marie Pédrot	2015-03-29
\| \| \| \| \|	The context matching function was dropping the surrounding context in let-ins.
*	Fixing bug #3900.	Pierre-Marie Pédrot	2015-02-11
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Avoiding introducing yet another convention in naming files.	Hugo Herbelin	2015-01-08