coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Interpretation et affichage corrects des notations LetTuple, affichage des ↵	herbelin	2004-08-23
\| \| \| \| \| \|	notations If git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6025 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #830 : les noms des implicites temporaires étaient inconnus ↵	herbelin	2004-08-23
\| \| \| \| \| \|	au moment de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Apply implicit types to local binders too	herbelin	2004-08-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6017 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 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
*	Suppression de Rawterm.loc, branchement sur Util.loc	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5911 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	Amélioration affichage coercions vers Funclass	herbelin	2004-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 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 sur commit 1.44 dans find_constructor (Not_Found pas rattrape)	herbelin	2004-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5640 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Heuristique pour traduire if-then-else quand le re-typage echoue	herbelin	2004-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5616 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵	herbelin	2004-03-28
\| \| \| \| \| \|	sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ↵	herbelin	2004-03-27
\| \| \| \| \| \|	ajout de la prise en compte dynamique des arguments scope pour les inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export compute_arguments_scope pour utilisation local a la construction des ↵	herbelin	2004-03-27
\| \| \| \| \| \|	inductifs et points fixes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5585 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
*	correction bug de facto des fix (2e)	barras	2004-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction bug de facto des fix	barras	2004-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction bug de choix de noms courts avec Suresnes/BDD	barras	2004-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug des points fixes (pb avec la contrib Matrices)	barras	2004-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un defaut dans la globalisation des variables de notations	herbelin	2004-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Branchement EmptyT, UnitT, IT vers leur equivalent dans Set	herbelin	2004-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5453 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction de bugs des points fixes	barras	2004-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5440 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
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵	herbelin	2004-03-02
\| \| \| \| \| \|	noms d'hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵	herbelin	2004-03-01
\| \| \| \| \| \|	des IntroPattern au parsing, à l'interprétation, à la traduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des implicites au travers des notations et abbreviations	herbelin	2004-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5394 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
*	Export des arguments scope au chargement, pas a l'ouverture (2eme)	herbelin	2004-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5369 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export des arguments scope au chargement, pas a l'ouverture	herbelin	2004-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5367 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
*	Bug coercions imbriquees + suppression des coercions avant filtrage sur ↵	herbelin	2004-02-18
\| \| \| \| \| \|	notations pour respecter le cpmt v7 et la symtrie avec le parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5357 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation erreur interp_notation	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5329 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation erreur interp_notation	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5324 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug affichage en presence de '{ _ }'	herbelin	2004-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
\| \| \| \| \| \| \| \| \| \| \|	notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A{B}+{C}" en présence d'une notation "_ { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A\|P}" etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Relachement condition pour afficher @ en cas d'explicitation d'implicites	herbelin	2004-02-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5285 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
*	Ajout option raw_print (Set Printing All) pour desactiver toute ↵	herbelin	2004-01-29
\| \| \| \| \| \|	fonctionnalite de haut niveau de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5269 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug activation erronée du traducteur en v8	herbelin	2004-01-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5257 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
*	Correction lecture des locations si pas demandees dans l'ordre	herbelin	2004-01-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5238 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export information des references de notations pour coqdoc	herbelin	2004-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5227 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
*	Traduction PolyList/List dans la qualification	herbelin	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5124 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Substitution dans REvar et PEvar plutot que encodage via noeud application ↵	herbelin	2003-12-19
\| \| \| \| \| \|	pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoin	herbelin	2003-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5098 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle tactique EExists	clrenard	2003-12-01
\| \| \| \| \| \| \|	Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7