coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot	2014-09-01
\|
*	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin	2014-08-18
\| \| \| \| \| \| \|	can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr.
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
\| \| \| \|	"pat/term" for "apply term on current_hyp as pat".
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications?
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
\| \| \| \| \|	This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
*	Faster uconstr.	Arnaud Spiwack	2014-08-01
\| \| \|	Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
\| \| \| \| \| \|	It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
*	Moving wit_unit to Stdarg.	ppedrot	2013-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16595 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving coercion functions out of Tacinterp.	ppedrot	2013-06-12
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16577 85f007b7-540e-0410-9357-904b9bb8a0f7