aboutsummaryrefslogtreecommitdiff
path: root/toplevel/himsg.mli
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-04commande Timeout + compaction des traces de debug_tacticbarras
2008-08-04Évolutions diverses et variées.herbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2006-02-07Amélioration des messages d'erreurs de tacred; unfold considère maintenant leherbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2004-07-16Nouvelle en-têteherbelin
2001-11-05GROS COMMIT:barras
2001-03-15entetesfilliatr
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
1999-12-13 - états fabriqués avec -silentfilliatr
1999-12-05premier debugagefilliatr
1999-12-03 - coqmktopfilliatr
1999-12-03modules profile, Coqinit et Coqtop (=main)filliatr
1999-09-19 - un effort sur la doc (ocamlweb)filliatr
1999-09-10affichage des erreurs de typage dans minicoqfilliatr
1999-09-08module Himsg, comme un foncteurfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 22:08:31 +0000