coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Typo (bug #797)	herbelin	2004-06-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5832 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Chgt role 2eme argument AList et implantation affichage motifs recursifs de ↵	herbelin	2004-04-08
\| \| \| \| \| \|	notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug protection array_fold_left2	herbelin	2004-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5536 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Motifs recursifs de notations: prise en compte de l'associativite et des ↵	herbelin	2004-03-17
\| \| \| \| \| \|	notations de pattern de filtrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5516 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
*	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
*	Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un ↵	herbelin	2004-02-03
\| \| \| \| \| \|	nom doit filtrer un nom et anonymous doit filtrer anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5280 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵	herbelin	2003-11-19
\| \| \| \| \| \|	dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation bug moins unaire (erreur de PP)	barras	2003-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug filtrage pour inversion notation	herbelin	2003-11-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4924 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout CPatNotation; renommage map_aconstr_with_binders_loc	herbelin	2003-11-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2003-09-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte d'un inductif sans argument dans le 'in' des 'match'	herbelin	2003-09-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4498 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin	2003-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 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
*	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
*	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
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 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 des scopes traversés dans les notations	herbelin	2002-12-15
\| \| \| \| \| \| \| \|	Traitement spécial pour le scope type_scope à l'internalisation Ajout "Locate Notation" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3441 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre les variables anonymes dans match_aconstr	herbelin	2002-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Préparation à la prise en compte des changements de scopes internes aux ↵	herbelin	2002-12-03
\| \| \| \| \| \|	notations; bugs d'affichage (confusion key/scope dans les délimiteurs); bug de non-indépendance des règles d'affichage et parsing vis à vis du nom des variables de la notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3365 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Re-déplacement du résultat de Grammar au niveau constr_expr	herbelin	2002-12-02
\| \| \| \| \| \| \| \| \| \|	(globalisation uniquement des noms - sauf cases, fix, ..., pas d'implicites, pas d'interprétation des scopes - pas plus robuste qu'avant...). Diverses améliorations affichage et parsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3350 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ne pas cacher les Metas d'une notations, ils peuvent être liant dans	herbelin	2002-11-26
\| \| \| \| \| \| \|	les filtrage de ltac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3302 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
*	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
*	Autoriser les abbreviations de Cases	herbelin	2002-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de Cases dans abbreviatable constr (aconstr) [utilisé dans la	herbelin	2002-11-18
\| \| \| \| \| \| \|	contrib Suresnes/MiniC]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3252 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à une représentation des fixpoints plus primitive dans constr_expr ↵	herbelin	2002-11-15
\| \| \| \| \| \|	(càd avec indices) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7