| Age | Commit message (Expand) | Author |
|---|
| 2004-01-26 | maj | filliatr |
| 2004-01-26 | maj | filliatr |
| 2004-01-24 | streamlines the keywords for definitions, require commandsbinders, notation | bertot |
| 2004-01-24 | maj | filliatr |
| 2004-01-23 | MAJ | herbelin |
| 2004-01-23 | Bug induction lors de types inductives avec parametres | herbelin |
| 2004-01-23 | maj | filliatr |
| 2004-01-22 | change add path commands to get the extra argument and the Hint commands | bertot |
| 2004-01-22 | Correction lecture des locations si pas demandees dans l'ordre | herbelin |
| 2004-01-22 | Protection table des locations lors de Load (pour coqdoc) | herbelin |
| 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-22 | maj | filliatr |
| 2004-01-22 | maj | filliatr |
| 2004-01-21 | MAJ | herbelin |
| 2004-01-21 | Export information des references et location de notations pour coqdoc | herbelin |
| 2004-01-21 | Export information des references de notations pour coqdoc | herbelin |
| 2004-01-21 | Deplacement lexer pour dependance dans constrintern | herbelin |
| 2004-01-21 | updates the structure of fix (struct argument added) and if | bertot |
| 2004-01-21 | MAJ | herbelin |
| 2004-01-21 | maj | filliatr |
| 2004-01-20 | coqide utf8 | marche |
| 2004-01-20 | Le traducteur utilisait un afficheur des reels obsolete et bugge | herbelin |
| 2004-01-20 | Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8 | herbelin |
| 2004-01-20 | maj | filliatr |
| 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-19 | maj | filliatr |
| 2004-01-17 | maj | filliatr |
| 2004-01-16 | ajoute une option -linkall dans compilation de bin/parser pour assurer que | bertot |
| 2004-01-16 | Corrige: Intros [] etait traduit intros (), qui ne reparse pas | barras |
| 2004-01-16 | maj | filliatr |
| 2004-01-15 | translation to structures now okay for pattern matching constructs | bertot |
| 2004-01-15 | Ajout nouvelles options | herbelin |
| 2004-01-15 | Ajout load-vernac-source-verbose | herbelin |
| 2004-01-15 | maj | filliatr |
| 2004-01-15 | maj | filliatr |
| 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-14 | make libraries, lexing of more utf8 symbols | marche |
| 2004-01-14 | maj | filliatr |
| 2004-01-13 | MAJ | herbelin |
| 2004-01-13 | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin |
| 2004-01-13 | Suppression de Rsyntax en v8 | herbelin |
