aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* - erreurs PretypeGravatar filliatr1999-12-10
* debug resetGravatar filliatr1999-12-10
* Suppression Rel de rawconstr et correction de bugs d'affichageGravatar herbelin1999-12-10
* debug discharge et inductifsGravatar filliatr1999-12-10
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* - constantes avec recettesGravatar filliatr1999-12-09
* Discharge (encore bugge)Gravatar filliatr1999-12-09
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
* initialisation load path (provisoire)Gravatar filliatr1999-12-06
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
* erreurs lexicalesGravatar filliatr1999-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
* Version initialeGravatar herbelin1999-12-02
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* module CommandGravatar filliatr1999-12-02
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* module MetasyntaxGravatar filliatr1999-12-01
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
* portage Vernacentries (debut)Gravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* portage modules Evarconv et EvarutilGravatar filliatr1999-11-29
* 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
* On se fait la main: plus de precision si ill-formed rec bodyGravatar herbelin1999-11-10
* module LogicGravatar filliatr1999-10-14
* deplacement des var. ex. dans proofsGravatar filliatr1999-10-08
* with_heavy_rollback deplace dans StatesGravatar filliatr1999-09-29
* corrections pour ocamlwebGravatar filliatr1999-09-28
* retablissement du toplevelGravatar filliatr1999-09-28
* module DeclareGravatar filliatr1999-09-19
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
* affichage des erreurs de typage dans minicoqGravatar filliatr1999-09-10
* documentation repertoire toplevelGravatar filliatr1999-09-10
* module Himsg, comme un foncteurGravatar filliatr1999-09-08
* minicoq: pretty-print applications; ambiguite grammaire supprimee; Ind, Const...Gravatar filliatr1999-09-08
* instanciation des opérateurs sur la bonne signature (celle deGravatar 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
* un mini toplevel pour tester le noyauGravatar filliatr1999-09-06