aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* 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
* MAJGravatar herbelin2004-02-03
* MAJGravatar herbelin2004-01-29
* MAJGravatar herbelin2004-01-23
* MAJGravatar herbelin2004-01-21
* *** empty log message ***Gravatar barras2003-12-23
* MAJGravatar herbelin2003-12-22
* *** empty log message ***Gravatar clrenard2003-12-01
* Nouvelle tactique EExistsGravatar clrenard2003-12-01
* Idtac parleGravatar narboux2003-12-01
* MAJGravatar herbelin2003-11-30
* MAJGravatar herbelin2003-11-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 11:16:58 +0000