| Commit message (Expand) | Author | Age |
* | 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-30 |
* | maj | filliatr | 2004-01-30 |
* | maj | filliatr | 2004-01-30 |
* | pour win32 | coq | 2004-01-29 |
* | Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit... | herbelin | 2004-01-29 |
* | Reparation d'une rupture (en presence de types implicites) de l'invariant que... | herbelin | 2004-01-29 |
* | pour ide sous windows | coq | 2004-01-29 |
* | MAJ | herbelin | 2004-01-29 |
* | Suppression de 'Print.' en v8 | herbelin | 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-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 |