aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Expand)AuthorAge
* Evd vient apres Environ -> id_of_existential expanseGravatar filliatr1999-11-26
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* Vernacinterp et Vernacentries (partiellement)Gravatar filliatr1999-11-24
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* module Tactics (debut)Gravatar filliatr1999-11-22
* module Pattern, Wcclausenv (interface) et TacticalsGravatar filliatr1999-11-19
* modules Bij, Gmapl, StockGravatar filliatr1999-11-19
* discriminations netsGravatar filliatr1999-11-19
* introduction de Gset et Gmap pour Tlm puis DnGravatar filliatr1999-11-18
* - répertoire tactics/Gravatar filliatr1999-10-22
* module Macros et TacinterpGravatar filliatr1999-10-22
* - module Redinfo dans library/ pour les constantes d'éliminationGravatar filliatr1999-10-22
* module Clenv (debut)Gravatar filliatr1999-10-20
* modules Evar_refiner et Typing_evGravatar filliatr1999-10-20
* module RefinerGravatar filliatr1999-10-19
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
* module Proof_treesGravatar filliatr1999-10-14
* - re-introduction d'une evar_map dans unsafe_envGravatar filliatr1999-10-13
* redeplacement des var. ex. dans kernel :-)Gravatar filliatr1999-10-13
* module LogicGravatar filliatr1999-10-12
* deplacement des var. ex. dans proofsGravatar filliatr1999-10-08
* corrections pour ocamlwebGravatar filliatr1999-09-28
* mise en place du toplevel (ne compile pas encore)Gravatar filliatr1999-09-28
* module DeclareGravatar filliatr1999-09-19
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
* module LibraryGravatar filliatr1999-09-18
* affichage des erreurs de typage dans minicoqGravatar filliatr1999-09-10
* modules System, Lib et StatesGravatar filliatr1999-09-10
* module HimsgGravatar filliatr1999-09-08
* compilation des grammaires (ouf)Gravatar filliatr1999-09-08
* - deplacement time stamps dans System (car utilise Unix)Gravatar filliatr1999-09-08
* modules Ast et PcoqGravatar filliatr1999-09-08
* mise a jourGravatar filliatr1999-09-07
* - minicoq : definition inductifs; syntaxe a->bGravatar filliatr1999-09-07
* mise en place commandes minicoqGravatar filliatr1999-09-07
* (debut) de grammaire minicoqGravatar filliatr1999-09-07
* mise en place grammaire minicoqGravatar filliatr1999-09-07
* mise en place repertoire test-suite/, toplevel/, parsing/Gravatar filliatr1999-09-06
* modules Libobject et Summary (partiel)Gravatar filliatr1999-09-03
* mise a jourGravatar filliatr1999-08-30
* module IndtypesGravatar filliatr1999-08-27
* environnement surGravatar filliatr1999-08-26
* le noyau compile et linkGravatar filliatr1999-08-26
* mise a jourGravatar filliatr1999-08-25
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
* machine: execute = typage avec universGravatar filliatr1999-08-20