| Commit message (Expand) | Author | Age |
* | Factorisation des produits de même type; parenthèses autour des x:=c et n:=... | herbelin | 2003-04-29 |
* | Ajout is_ident_tail | herbelin | 2003-04-29 |
* | Localisation erreurs TacAlias; Globalisation moins tolérante dans les | herbelin | 2003-04-28 |
* | Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix... | herbelin | 2003-04-27 |
* | Reparation affichage LetTac | herbelin | 2003-04-27 |
* | extension des caracteres UTF 8 autorises dans les symboles | filliatr | 2003-04-25 |
* | Ajout "at next level" dans Notation | herbelin | 2003-04-17 |
* | simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis... | letouzey | 2003-04-16 |
* | Localisation des appels de tactiques définies sans arguments | herbelin | 2003-04-14 |
* | Correction bug PR#278 | coq | 2003-04-14 |
* | Ajout option 'Local' à Infix et Notation | herbelin | 2003-04-11 |
* | Affichage forcé des implicites contextuels si pas de contexte connu | herbelin | 2003-04-10 |
* | Réorganisation de Impargs + mise en place d'une infrastructure | herbelin | 2003-04-09 |
* | Ajout option "Local" à "Open Scope" | herbelin | 2003-04-08 |
* | lconstr pour genterm en v8 | herbelin | 2003-04-07 |
* | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin | 2003-04-07 |
* | Ajout cas Match | herbelin | 2003-04-07 |
* | Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite | herbelin | 2003-04-07 |
* | Options d'affichage maintenant dans Constrextern | herbelin | 2003-04-07 |
* | espace manquant | herbelin | 2003-04-02 |
* | Ajout d'un message à FailTac | herbelin | 2003-03-31 |
* | Bug pattern_occ_hyp_list | herbelin | 2003-03-31 |
* | Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar) | herbelin | 2003-03-29 |
* | notations <>, Assumption avec existentiel, replace term | mohring | 2003-03-28 |
* | MAJ des mots-clés, Definition, Theorem, ... | herbelin | 2003-03-27 |
* | MAJ des mots-clés, Definition, Theorem, ... | herbelin | 2003-03-27 |
* | Affinement nommage des productions | herbelin | 2003-03-27 |
* | *** empty log message *** | barras | 2003-03-21 |
* | reparations suite a la nouvelle syntaxe: | barras | 2003-03-14 |
* | Ajout réaffichage SubClass | herbelin | 2003-03-13 |
* | *** empty log message *** | barras | 2003-03-12 |
* | Renommage indpar pour usage plus general | herbelin | 2003-03-12 |
* | Bug délimiteur de scope en vieil affichage ast | herbelin | 2003-03-04 |
* | Retour vieil afficheur | herbelin | 2003-03-03 |
* | Interpretation des entiers dans les reels via les scopes | desmettr | 2003-02-27 |
* | Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'... | herbelin | 2003-02-27 |
* | Correction test token normal | herbelin | 2003-02-27 |
* | Le lexeur et Notation savent reconnaître si un unicode des blocs | herbelin | 2003-02-27 |
* | Retour nouvel afficheur | herbelin | 2003-02-27 |
* | Affinement entree annot | herbelin | 2003-02-17 |
* | Debugger plus informatif | delahaye | 2003-02-13 |
* | Ajout du traducteur | desmettr | 2003-02-05 |
* | Pour satisfaire ProofGeneral | coq | 2003-01-31 |
* | Adds a possibility to construct a term as if it had been parsed through | bertot | 2003-01-30 |
* | Deux p\'tits trucs ;) | coq | 2003-01-27 |
* | I changed the interface to make sure SearchAbout is defined according to | bertot | 2003-01-22 |
* | Restructuration interpréteur de tactique: plus d'évaluation partielle à la... | herbelin | 2003-01-19 |
* | Rétablissement pr_pattern | herbelin | 2003-01-19 |
* | Bugs affichage | herbelin | 2003-01-16 |
* | Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un... | herbelin | 2003-01-15 |