| Commit message (Expand) | Author | Age |
* | Nametab data structure reorganisation | coq | 2002-09-24 |
* | La notation with dependante + affichage dependante de moduels corrige | coq | 2002-09-20 |
* | Pretty-printing preliminaire des modules, commandes | coq | 2002-08-19 |
* | Strengthenning rules for modules + No modules in sections | coq | 2002-08-16 |
* | Petites corrections ici et la | coq | 2002-08-13 |
* | Modules dans COQ\!\!\!\! | coq | 2002-08-02 |
* | Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour | herbelin | 2002-07-11 |
* | Ajout de FNL ou utilisation de msgnl | herbelin | 2002-06-07 |
* | Intgration uniforme de coercions dans les dclarations (Variable and co) et re... | herbelin | 2002-06-03 |
* | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
* | Plusieurs arguments autorisés pour Require et Read Module | herbelin | 2002-01-18 |
* | Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress... | herbelin | 2001-12-16 |
* | compat ocaml 3.03 | filliatr | 2001-12-13 |
* | - condition de garde (suite) | barras | 2001-12-10 |
* | reparation de Locate | barras | 2001-11-29 |
* | nouvel algo de conversion plus uniforme | barras | 2001-11-29 |
* | Diverses petites simplications de la machine de preuves. | clrenard | 2001-11-19 |
* | Choucroute entre les tables de synchronisation, les options -silent et les et... | letouzey | 2001-11-08 |
* | GROS COMMIT: | barras | 2001-11-05 |
* | Reorganisation de Goption. Passage des options l'utilisant en synchrone | letouzey | 2001-10-30 |
* | Abstraction de l'immplementation de dirpath et implementation dans l'autre se... | herbelin | 2001-10-17 |
* | Amélioration mise en page Print ML Module et Print ML Module | herbelin | 2001-10-17 |
* | Suppression option immediate_discharge; nettoyage de Declare et conséquences | herbelin | 2001-10-11 |
* | Réparation des options Set Printing and co | herbelin | 2001-09-21 |
* | Mise en place globalisation optionnelle pour Infix/Distfix | herbelin | 2001-09-21 |
* | Protection contre Not_found | herbelin | 2001-09-21 |
* | Correction bug affichage Infix/Distfix | herbelin | 2001-09-20 |
* | Transparent | barras | 2001-09-20 |
* | Blindage de Show Intro | letouzey | 2001-09-17 |
* | Suppression des library roots, on teste si un nom est absolu autrement | herbelin | 2001-09-07 |
* | Parsing | herbelin | 2001-08-10 |
* | ajout Show Intro(s) | letouzey | 2001-07-04 |
* | Facilites pour le debogguage des univers. | coq | 2001-05-29 |
* | Pretty -> Prettyp | filliatr | 2001-05-28 |
* | amelioration des messages d'erreurs vis a vis des evars | barras | 2001-05-23 |
* | Retire commenatires obsoletes | mohring | 2001-04-20 |
* | un typage sûr pour Goal et Check | filliatr | 2001-04-20 |
* | Cd est silencieux si -silent | filliatr | 2001-04-19 |
* | Uniformisation des 'Save def_tok id' | herbelin | 2001-04-09 |
* | Add a Comments command, that does nothing, but is quite useful to to have | bertot | 2001-04-04 |
* | utilisation de Options.if_verbose | filliatr | 2001-04-03 |
* | amelioration de la structure des univers | barras | 2001-03-28 |
* | entetes | filliatr | 2001-03-15 |
* | protection contre certaines exceptions levees par marshal_{in,out} | barras | 2001-03-09 |
* | Déplacement de qualid dans Nametab, hors du noyau | herbelin | 2001-03-01 |
* | ident au lieu de string pour le nom de base de qualid | herbelin | 2001-02-16 |
* | Prise en compte noms longs dans Implicits | herbelin | 2001-02-16 |
* | Theoreme opaques | mohring | 2001-02-12 |
* | Scratch par defaut si rien n'est specifier dans Add LoadPath | herbelin | 2001-02-08 |
* | Meilleure approche du conflit path/freeze/library_root en séquentialisant la... | herbelin | 2001-02-07 |