coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Conséquences nettoyage pretyping.ml	herbelin	2005-09-09
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Nouvelle en-tête	herbelin	2004-07-16
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin	2004-03-27
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...	herbelin	2003-10-14
*	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin	2003-10-08
*	cosmetique	herbelin	2003-09-06
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Mécanisme plus simple et efficace pour traduire les implicites	herbelin	2003-04-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Implicit Variables Type dans les inductive	herbelin	2003-03-29
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Prise en compte des scopes traversés dans les notations	herbelin	2002-12-15
*	Re-déplacement du résultat de Grammar au niveau constr_expr	herbelin	2002-12-02
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14