coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fusion des g_syntaxnew.ml avec les g_syntax.ml avec sélection dynamique selon	herbelin	2003-09-12
\| \| \| \| \| \| \|	l'option v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4385 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4378 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ module requis pour le parsing des numéraux	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4377 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des scopes d'arguments	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage des projections au niveau 1	herbelin	2003-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 85f007b7-540e-0410-9357-904b9bb8a0f7
*	9 est associatif a gauche	herbelin	2003-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4348 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction de Distfix	herbelin	2003-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4344 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout construction If primitive dans constr_expr et rawconstr	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'Grammar tactic' devient 'Tactic Notation'	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction des réferences arguments de commandes non primitives	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4331 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code mort	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4329 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place possibilité de définitions locales dans les paramètres des ↵	herbelin	2003-09-06
\| \| \| \| \| \|	records en v7 aussi git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4324 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place possibilité de définitions locales dans les paramètres des ↵	herbelin	2003-09-06
\| \| \| \| \| \|	records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'Implicits qid' -> 'Implicit Arguments qid'	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4320 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adapter l'entree de grammaire a la version 7 ou 8	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4317 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place possibilité de définitions locales dans les paramètres des ↵	herbelin	2003-09-06
\| \| \| \| \| \|	inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4313 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
\| \| \| \| \| \| \| \|	et tactiques; qqes bugs d'affichage; passage de la précédence des projections de 10 à 9 avec associativité à gauche git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug affichage tactiques supplementaires en v8 (suite)	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4311 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug affichage tactiques supplementaires en v8	herbelin	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4310 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Impression sans ',' des constructeurs de meme type, pour v8	herbelin	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4301 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Relachement conflit 'with' dans le cas des Module with Definition	herbelin	2003-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4295 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'Assumptions' sur le modèle général des lieurs	herbelin	2003-08-31
\| \| \| \| \| \| \|	Syntaxe à la ML pour les constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4284 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des inductifs en v8	herbelin	2003-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4281 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pb de mot-cle	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4272 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout token '!' pour correctness	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4269 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Enregistrement tuple_constr	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4268 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug compilation	herbelin	2003-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4192 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'	herbelin	2003-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4184 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option Local aux Hint	herbelin	2003-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4175 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Token '.(' seulement pour v8, sinon conflit avec '.(*'	herbelin	2003-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4137 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
*	freshid -> fresh	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4127 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tables logarithmiques pour les coercions + nettoyage	herbelin	2003-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug	herbelin	2003-05-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4081 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout FreshId	herbelin	2003-05-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4072 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout V8Notation	herbelin	2003-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4061 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵	herbelin	2003-05-21
\| \| \| \| \| \|	les metavariables de patterns; réparation local défs récursive dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵	herbelin	2003-05-21
\| \| \| \| \| \|	les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Possibilité de syntaxe conjointement à la définition des inductifs et des ↵	herbelin	2003-05-21
\| \| \| \| \| \|	points-fixes; prise en compte par le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4042 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
\| \| \| \| \| \| \| \| \|	Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petite correction d'affichage de modules	coq	2003-05-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3996 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin	2003-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3984 85f007b7-540e-0410-9357-904b9bb8a0f7