| Age | Commit message (Expand) | Author |
|---|
| 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 | petit bug avec Extraction Optimize | letouzey |
| 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-10 | Correction of a bug in Functional Scheme discovered when porting the | coq |
| 2004-02-09 | New version of Functional Scheme and functional induction. Deals with | coq |
| 2004-02-06 | correction de bugs de congruence et firstorder (inductifs) | corbinea |
| 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 |
| 2004-01-22 | change add path commands to get the extra argument and the Hint commands | bertot |
| 2004-01-22 | fixes argument lists for tactic definitions, updates inversion tactics | bertot |
| 2004-01-22 | adds a clause argument to symmetry | bertot |
| 2004-01-22 | corrects the way the structural argument declaration is handled in | bertot |
| 2004-01-22 | adds the notations in inductive definitions, improves the consistency between | bertot |
| 2004-01-22 | handles explicit function calls, names meta variables in patterns | bertot |
| 2004-01-21 | updates the structure of fix (struct argument added) and if | bertot |
| 2004-01-19 | handles projector notations, cases with return types, | bertot |
| 2004-01-19 | 1.20 | bertot |
| 2004-01-19 | 1.19 | bertot |
| 2004-01-19 | adds constructs to handle notations in patterns | bertot |
| 2004-01-15 | translation to structures now okay for pattern matching constructs | bertot |
| 2004-01-14 | compact nested universal quantifications into a single quantification with | bertot |
| 2004-01-14 | make sure the parser for FORMULA does not require them to be enclosed in | bertot |
| 2004-01-14 | Now, the grammar extension from .v files are concentrated in just a few | bertot |
| 2004-01-13 | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-12-24 | Parenthesage du terme pour accepter 'of' comme non ident | herbelin |
| 2003-12-24 | La correction precedente a mis en evidence un defaut de l'utilisation de intr... | herbelin |
| 2003-12-23 | 'of' restait par erreur mot-cle dans psyntax.ml4 en v8 | herbelin |
| 2003-12-23 | Retablissement de GIntuition juste pour FSets | herbelin |
| 2003-12-23 | *** empty log message *** | barras |
