aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.mli
Commit message (Expand)AuthorAge
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* GROS COMMIT:Gravatar barras2001-11-05
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* premier debugageGravatar filliatr1999-12-05
* - coqmktopGravatar filliatr1999-12-03
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
* affichage des erreurs de typage dans minicoqGravatar filliatr1999-09-10
* module Himsg, comme un foncteurGravatar filliatr1999-09-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 14:01:45 +0000