aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
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
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
2004-11-17Ajout 'Locate Module'herbelin
2004-11-09MAJherbelin
2004-11-08Prise en compte des notations récursives dans l'option 'format'herbelin
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...herbelin
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
2004-04-17Incorrection exportation XMLherbelin
2004-04-17Finalement pas de liste des contributions (cela n'avait été fait que pour l...herbelin
2004-04-16Nouvelles majsherbelin
2004-04-14MAJherbelin
2004-03-28MAJherbelin
2004-03-17MAJherbelin
2004-03-15preparation pour release (suite)barras
2004-03-15MAJherbelin
2004-03-10MAJherbelin
2004-02-27MAJherbelin
2004-02-21MAJherbelin
2004-02-12MAJherbelin
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
2004-02-06MAJherbelin
2004-02-03MAJherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 11:36:56 +0000