coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
\| \| \| \| \| \| \| \| \|	Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin	2007-04-18
\| \| \| \| \| \| \| \| \| \| \|	(les let-in étaient comptés comme des produits, introduisant une incohérence sur le nombre de produits à instancier dans les lemmes appelés par apply). - Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition. - Doc développeur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ fichier dev/doc/changes.txt	herbelin	2006-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8946 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTEND	herbelin	2006-05-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration dossier dev et mise à jour de certaines documentations	herbelin	2006-05-23
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7