coq - The formal proof system

Age	Commit message (Collapse)	Author
2002-03-26	Prise en compte des dependances dans la tactique Case	mohring
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21	Décomposition de l'application n-aire en application binaire pour que ↵	herbelin
	Pattern réussisse sur des motifs partiellement appliqués git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2560 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04	Nouveau Rewrite-in plus economique	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15	petits changements cosmetiques sur les tactiques	barras
	+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-11	substitution et pattern modulo let	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07	petit nettoyage de kernel/inductive	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-17	Amélioration affichage échec lookup_eliminator	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2403 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13	compat ocaml 3.03	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05	GROS COMMIT:	barras
	- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7