coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Restructuration fonctions de réécriture depuis égalité dépendante; ↵	herbelin	2004-10-27
\| \| \| \| \| \|	factorisation cut_replacing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6261 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplifications concommitantes à la correction du bug #855	herbelin	2004-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6126 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
*	Suppression de la distinction entre elimination de Type vers Type ou pas ↵	herbelin	2004-03-11
\| \| \| \| \| \|	(False, eq, Unit ont maintenant les bonnes proprietes pour fonctionner partout) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5454 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'replace in'	herbelin	2004-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5408 85f007b7-540e-0410-9357-904b9bb8a0f7
*	factorisation et generalisation des clauses	barras	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4596 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau Subst:	barras	2002-12-17
\| \| \| \| \| \| \| \|	- marche lorsqu'il n'y rien a reecrire - marche avec les hypotheses definies (Subst inclut l'Unfold partout) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Subst (tout court)	filliatr	2002-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3007 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tactique Subst x1 ... xn	filliatr	2002-09-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2998 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code mort de AutoRewrite	herbelin	2002-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2993 85f007b7-540e-0410-9357-904b9bb8a0f7
*	AutoRewrite substitutive...	coq	2002-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2965 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tactique Subst	filliatr	2002-07-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2894 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Repercussion de la possibilit de mettre des hyps quantifiees dans ↵	herbelin	2002-06-05
\| \| \| \| \| \|	Simplify_eq et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq ↵	herbelin	2002-06-05
\| \| \| \| \| \|	et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Centralisation des références à des globaux de Coq dans Coqlib ↵	herbelin	2001-02-14
\| \| \| \| \| \|	(ex-Stdlib) et suppression Stock git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1386 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage	herbelin	2000-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@439 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du langage de tactiques	delahaye	2000-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrage	herbelin	2000-04-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@389 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement du type reference dans Term	herbelin	2000-04-28
\| \| \| \| \| \| \| \| \|	Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@384 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de type_of_case, type_case_branches, etc;nettoyage	herbelin	2000-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@350 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
	- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7