coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	'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
*	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@4319 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cosmetique	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4318 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
*	Pour accomoder autant le printer v8 que v7	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4315 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre les types sans corps associé	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4314 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
*	principes de récurrences plus efficaces pour l'extraction	letouzey	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4309 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zdiv plus efficace: r+r -> 2*r	letouzey	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4308 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zabs_Zsgn	letouzey	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4307 85f007b7-540e-0410-9357-904b9bb8a0f7
*	highlighting de Extraction	letouzey	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4306 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug dans calcul nb d'occurrences	letouzey	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4305 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affichage de la nature des colonnes	filliatr	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4304 85f007b7-540e-0410-9357-904b9bb8a0f7
*	install coqwc	filliatr	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4303 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqwc	filliatr	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4302 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
*	Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'	herbelin	2003-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4300 85f007b7-540e-0410-9357-904b9bb8a0f7
*	option pour supprimer les menus contextuels sur les buts	marche	2003-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4299 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Projections	herbelin	2003-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4298 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2003-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4297 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4296 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
*	Contorsions pour que l'interpretation deses foncteurs depende des parametres ↵	herbelin	2003-09-02
\| \| \| \| \| \|	de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4294 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Freeze mal place	herbelin	2003-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4293 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export process_module_bindings pour traducteur	herbelin	2003-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4292 85f007b7-540e-0410-9357-904b9bb8a0f7
*	auto completion disabled par defaut	marche	2003-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug traduction Search, SearchPattern, etc.	herbelin	2003-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4290 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de passage du scope tmp sous les lambdas	herbelin	2003-09-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4289 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de 'relation' à Type	herbelin	2003-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4288 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4287 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe des constructeurs et des hypotheses	herbelin	2003-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4286 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug et améliorations divers	herbelin	2003-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4285 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
*	Symetrisation des changements implicites de scope	herbelin	2003-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4283 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ↵	herbelin	2003-08-31
\| \| \| \| \| \|	\| S (n:nat)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4282 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
*	V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclass	herbelin	2003-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4280 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction d'un stack overflow possible (PR#320)	letouzey	2003-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4278 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-08-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4277 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion -translate et -ftranslate	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traducteur de correctness	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4275 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4274 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction mlnames	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4273 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
*	Amélioration affichage syntaxe modules	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Positionnement precoce de l'option -v7	herbelin	2003-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4270 85f007b7-540e-0410-9357-904b9bb8a0f7