| Commit message (Expand) | Author | Age |
* | updates the tactics contradiction and autorewrite, the commands | bertot | 2004-01-29 |
* | maj | filliatr | 2004-01-29 |
* | Bug de Require multiple | herbelin | 2004-01-28 |
* | make sure that 'in' clauses for reduction tactics are translated | bertot | 2004-01-28 |
* | maj | filliatr | 2004-01-28 |
* | maj | filliatr | 2004-01-28 |
* | Bug activation erronée du traducteur en v8 | herbelin | 2004-01-27 |
* | meilleure separation de compil et install de coq, coqide et coq-interface | barras | 2004-01-27 |
* | Correction des cibles des theories indviduelles | herbelin | 2004-01-27 |
* | MAJ simplification | herbelin | 2004-01-27 |
* | Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ... | herbelin | 2004-01-27 |
* | Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ... | herbelin | 2004-01-27 |
* | maj | filliatr | 2004-01-27 |
* | maj | filliatr | 2004-01-27 |
* | deplacement des cma et cmxa dans les sous-repertoires | barras | 2004-01-26 |
* | reparation de qqs bugs du traducteur | barras | 2004-01-26 |
* | a try to make intro patterns better | bertot | 2004-01-26 |
* | maj | filliatr | 2004-01-26 |
* | maj | filliatr | 2004-01-26 |
* | streamlines the keywords for definitions, require commandsbinders, notation | bertot | 2004-01-24 |
* | maj | filliatr | 2004-01-24 |
* | MAJ | herbelin | 2004-01-23 |
* | Bug induction lors de types inductives avec parametres | herbelin | 2004-01-23 |
* | maj | filliatr | 2004-01-23 |
* | 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-22 |
* | 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-21 |
* | 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-20 |
* | 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-19 |