aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2006-06-15MAJherbelin
2006-06-14MAJherbelin
2006-06-12git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 85f007b7-540e-04...jforest
2006-06-09Nouvelle MAJherbelin
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
2006-06-08nouvelle MAJherbelin
2006-06-07replace byherbelin
2006-06-07Ajout Whelpherbelin
2006-05-23MAJherbelin
2006-05-18ajout de mes modifs recentesletouzey
2006-05-10Centralisation de la détection lettre/symbole par le lexeur dans les plages ...herbelin
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-04-11ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)courtieu
2006-03-05MAJherbelin
2006-02-23Ajout 'exists! x:A, Pherbelin
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
2006-02-07Idem numbering of 'Unfold', 'simpl', ...herbelin
2006-02-07Mise en conformité de l'ordre des occurrences de pattern avec l'affichageherbelin
2006-02-07MAJherbelin
2006-02-06coq_makefileherbelin
2006-01-29MAJ (synonymes de Lemma; auto using)herbelin
2006-01-19Export eassumptionherbelin
2006-01-19Extended Unicode supportherbelin
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomherbelin
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
2006-01-07MAJherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur; changeme...herbelin
2005-12-23*** empty log message ***herbelin
2005-12-21MAJherbelin
2005-09-09Declare Implicit Tacticherbelin
2005-07-15add a left and right tactic for classical logicnarboux
2005-07-15foldherbelin
2005-06-22Added entry constr_may_eval for tactic extensions (new syntax)herbelin
2005-05-26New environment variable COQREMOTEBROWSER to set the command used by Coqsacerdot
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
2005-05-18Implemented autorewrite with ... in hyp [using ...].sacerdot
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-09possibilité d'écrire [foo| ] au lieu de [foo|idtac]letouzey
2005-04-26Fixed hypotheses of Z_lt_induction (see #957)herbelin
2005-03-29Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...herbelin
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the s...herbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
2005-01-03HUGE COMMITsacerdot
2004-12-27Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 15:22:46 +0000