aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Expand)AuthorAge
* debug resetGravatar filliatr1999-12-10
* Suppression Rel de rawconstr et correction de bugs d'affichageGravatar herbelin1999-12-10
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* Ajout option spéciale PPCGravatar herbelin1999-12-06
* premier debugageGravatar filliatr1999-12-05
* compilation nativeGravatar filliatr1999-12-03
* bug make_strength repareGravatar filliatr1999-12-03
* - coqmktopGravatar filliatr1999-12-03
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
* - global_reference traite des variablesGravatar filliatr1999-12-03
* Modifs suite à intégration de class.mlGravatar herbelin1999-12-02
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* poursuite de VernacentriesGravatar filliatr1999-12-01
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
* printersGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* portage modules Evarconv et EvarutilGravatar filliatr1999-11-29
* portage Astterm (partiellement)Gravatar filliatr1999-11-29
* fin Recordops, et debut EvarutilGravatar filliatr1999-11-27
* Modification pour faire compiler pretyping.ml qui maintenant compileGravatar herbelin1999-11-26
* module Classops; ajout de fonctions dans Declare en consequenceGravatar filliatr1999-11-26
* prvectiGravatar filliatr1999-11-26
* module TermastGravatar filliatr1999-11-26
* 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