aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.mli
Commit message (Expand)AuthorAge
* Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalGravatar letouzey2013-03-14
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Noise for nothingGravatar pboutill2012-03-02
* Finish branching functions handling module errors (cf. r13886)Gravatar letouzey2011-03-16
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* 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-12-13 04:35:16 +0000