| Age | Commit message (Expand) | Author |
|---|
| 2004-11-29 | Commit précédent erroné; retour version précédente | herbelin |
| 2004-11-28 | MAJ vis à vis de extratactics | herbelin |
| 2004-11-17 | Locate Module | herbelin |
| 2004-11-17 | New command "Print Rewrite HindDb dbname". | sacerdot |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-10-11 | 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval... | herbelin |
| 2004-09-17 | restructuration des printers: proofs passe avant parsing | barras |
| 2004-09-09 | Ajout de or-pattern pour le match-with v8 | herbelin |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
| 2004-07-23 | "Show Setoids" command added. | sacerdot |
| 2004-07-18 | Abstraction vis a vis du type loc pour ocaml 3.08 | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-06-29 | moved instantiate binding to extratactics | corbinea |
| 2004-06-29 | License de contrib/interface | herbelin |
| 2004-06-28 | contrib/interface *$*$@! | corbinea |
| 2004-04-21 | pb install de pcoq | barras |
| 2004-03-15 | preparation pour release (suite) | barras |
| 2004-03-15 | To make that the translation process does not fail on data produced by | bertot |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-03-03 | takes better account of the new possibility to pass a parametric count argument | bertot |
| 2004-03-03 | removes capital letters in two tactic names. | bertot |
| 2004-03-03 | make sure the implicit argument indications are in the right order | bertot |
| 2004-03-02 | Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no... | herbelin |
| 2004-03-02 | Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va... | herbelin |
| 2004-03-01 | Ajout IntroPattern comme type d'argument générique | herbelin |
| 2004-02-26 | Keep structure information for Fixpoint declaration and Fix terms | bertot |
| 2004-02-26 | Not all cases for coercions and locality were handled | bertot |
| 2004-02-23 | corrects the treatement of SubClass declarations | bertot |
| 2004-02-19 | makes sure the following examples are well-treated: | bertot |
| 2004-02-18 | - fixed the Assert_failure error in kernel/modops | barras |
| 2004-02-16 | accomodate the .. extension | bertot |
| 2004-02-16 | adds a new command for searching a pattern inside the premises of theorems | bertot |
| 2004-02-16 | corrects a bug in name reservation, simplifies or_intro, removes dead code | bertot |
| 2004-02-13 | adds a new command add_rec_path for the parser program and changes add_path | bertot |
| 2004-02-13 | adds the possibility to have terms (and not just identifiers) as hints | bertot |
| 2004-02-13 | adds the possibility to have terms (and not just identifiers) as hints | bertot |
| 2004-02-12 | lazy was translated to cbv, obviously wrong | bertot |
| 2004-02-12 | Implicits can have an optional list of argument, which is different | bertot |
| 2004-02-11 | a new version that uses intro patterns, but the code still needs some cleaning | bertot |
| 2004-02-11 | removes a lot comments that may be useful for later code maintenance, but | bertot |
| 2004-02-02 | adds the possibility to mark function arguments as formulas in Ltac | bertot |
| 2004-02-02 | adds the possibility to mark function arguments as formulas in Ltac | bertot |
| 2004-01-30 | updates the definition of tactics using Ltac and adds the subst tactic | bertot |
| 2004-01-30 | adds module commands and update the extration command | bertot |
| 2004-01-29 | Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :... | herbelin |
| 2004-01-29 | updates the tactics contradiction and autorewrite, the commands | bertot |
| 2004-01-28 | make sure that 'in' clauses for reduction tactics are translated | bertot |
| 2004-01-26 | a try to make intro patterns better | bertot |
| 2004-01-24 | streamlines the keywords for definitions, require commandsbinders, notation | bertot |
