coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- make the modifiers "value of" and "type of" for "set" working (it was not!), - clear unselected hypotheses in the "in" clause of "induction/destruct" when the destructed term is a variable (experimental), - support for generalization of hypotheses in the induction hypotheses using the "in" clause of "induction" (e.g. "induction n in m, H" will generalize over m -- would it be better to have an explicit "over"/"generalizing" clause ?). Added clause "as" to "apply in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	more evar stuff	corbinea	2004-06-28
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7