aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* coq_makefileGravatar herbelin2006-02-06
* MAJ (synonymes de Lemma; auto using)Gravatar herbelin2006-01-29
* Export eassumptionGravatar herbelin2006-01-19
* Extended Unicode supportGravatar herbelin2006-01-19
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomGravatar herbelin2006-01-16
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* Ajout paramétricité du nom de la base de hint dans auto et trivialGravatar herbelin2006-01-11
* MAJGravatar herbelin2006-01-07
* Suppression des parseurs et printeurs v7; suppression du traducteur; changeme...Gravatar herbelin2005-12-26
* *** empty log message ***Gravatar herbelin2005-12-23
* MAJGravatar herbelin2005-12-21
* Declare Implicit TacticGravatar herbelin2005-09-09
* add a left and right tactic for classical logicGravatar narboux2005-07-15
* foldGravatar herbelin2005-07-15
* Added entry constr_may_eval for tactic extensions (new syntax)Gravatar herbelin2005-06-22
* New environment variable COQREMOTEBROWSER to set the command used by CoqGravatar sacerdot2005-05-26
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* possibilité d'écrire [foo| ] au lieu de [foo|idtac]Gravatar letouzey2005-05-09
* Fixed hypotheses of Z_lt_induction (see #957)Gravatar herbelin2005-04-26
* Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...Gravatar herbelin2005-03-29
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* HUGE COMMITGravatar sacerdot2005-01-03
* Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)Gravatar herbelin2004-12-27
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
* MAJGravatar herbelin2004-11-09
* Prise en compte des notations récursives dans l'option 'format'Gravatar herbelin2004-11-08
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
* Incorrection exportation XMLGravatar herbelin2004-04-17
* Finalement pas de liste des contributions (cela n'avait été fait que pour l...Gravatar herbelin2004-04-17
* Nouvelles majsGravatar herbelin2004-04-16
* MAJGravatar herbelin2004-04-14
* MAJGravatar herbelin2004-03-28
* MAJGravatar herbelin2004-03-17
* preparation pour release (suite)Gravatar barras2004-03-15
* MAJGravatar herbelin2004-03-15
* MAJGravatar herbelin2004-03-10
* MAJGravatar herbelin2004-02-27
* MAJGravatar herbelin2004-02-21
* MAJGravatar herbelin2004-02-12
* New version of Functional Scheme and functional induction. Deals withGravatar coq2004-02-09
* MAJGravatar herbelin2004-02-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 04:23:32 +0000