coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
*	Hack peu élégant pour permettre de parser des listes avec séparateurs dans	herbelin	2006-10-24
*	Suppresion redondance interp_entry_name entre Q_util et Argextend	herbelin	2006-06-23
*	Changement du type d'argument 'TacticArgType X' en un type	herbelin	2006-06-08
*	Petite correction nom QuantHypArgType suite suppression traducteur	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	* empty log message *	barras	2005-11-18
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06
*	Abstraction vis à vis de dummy_loc	herbelin	2004-07-20
*	Nouvelle en-tête	herbelin	2004-07-16
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	Nouvelle syntaxe à la ML pour donner le type ML des extensions d'arguments	herbelin	2004-06-17
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin	2004-03-01
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	* empty log message *	barras	2003-03-12
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin	2002-06-05