coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵	herbelin	2005-12-30
\| \| \| \| \| \|	de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement des named_context	gregoire	2005-12-02
\| \| \| \| \| \| \| \|	Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affinements suite à extension Tactic Notation aux tacticielles	herbelin	2005-05-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7030 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵	herbelin	2005-05-17
\| \| \| \| \| \|	aux niveaux syntaxiques des tacticielles + erreur typage TacAlias git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7028 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des Tactic Notation	herbelin	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵	herbelin	2005-01-02
\| \| \| \| \| \|	printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage d'une bibliothèque de grands entiers naturels vers une ↵	herbelin	2004-12-25
\| \| \| \| \| \|	bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6505 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug Notation: il faut re-déclarer les règles de parsing des ↵	herbelin	2004-11-22
\| \| \| \| \| \|	notations au moment de la déclaration d'interprétation car la règle de parsing peut être dans un autre fichier qui n'est pas importé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6340 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
*	Mise en place de motifs récursifs dans Notation; quelques simplifications ↵	herbelin	2004-03-17
\| \| \| \| \| \|	au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modif des fixpoints pour que si on donne une notation au produit, les pts ↵	barras	2004-03-05
\| \| \| \| \| \|	fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin	2004-03-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
\| \| \| \| \| \| \| \| \|	- fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
\| \| \| \| \| \| \| \|	dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation de qqs bugs du traducteur	barras	2004-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle solution pour le probleme d'effacement des niveaux vides de ↵	herbelin	2003-11-20
\| \| \| \| \| \|	operconstr et pattern: plus de niveaux vides git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4956 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre l'effacement des niveaux vides de operconstr et pattern ↵	herbelin	2003-11-19
\| \| \| \| \| \|	par le delete_rule de camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4947 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar	herbelin	2003-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	En v8, une notation, c'est 2 regles et un niveau	herbelin	2003-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4795 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	On n'autorise plus les niveaux doubles L/R en v8	herbelin	2003-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4670 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 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
*	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
*	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
*	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
*	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
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
\| \| \| \| \| \| \|	définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵	letouzey	2003-04-16
\| \| \| \| \| \|	list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte notations dans les extensions de motiff	herbelin	2002-12-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Meilleure factorisation des entrées NEXT internes	herbelin	2002-12-15
\| \| \| \| \| \| \| \|	Nouvelle entrée "annot" pour contourner le conflit entre ">" et les annotations entre piquants git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3440 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug de non-indépendance des règles d'affichage et parsing vis à vis du ↵	herbelin	2002-12-03
\| \| \| \| \| \|	nom des variables de la notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3367 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7
*	On force l'associativité pour les entrées sans niveaux	herbelin	2002-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3348 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Synchro level (suite)	herbelin	2002-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3347 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de Snext pour gérer les symboles non associatifs	herbelin	2002-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3343 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Synchro de la table des niveaux avec les sections	herbelin	2002-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3341 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affinement de la gestion des niveaux toujours; type ETBigint	herbelin	2002-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affinement encore	herbelin	2002-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3316 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affinement de la gestion des niveaux	herbelin	2002-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3314 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction sur commit précédent	herbelin	2002-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3307 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin	2002-11-26
\| \| \| \| \| \| \| \|	Affinement de la gestion des niveaux de constr. Cablage en dur du parsing et de l'affichage des délimiteurs de scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ delimiters et niveaux d'associativite	herbelin	2002-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3281 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵	herbelin	2002-11-24
\| \| \| \| \| \|	améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7