aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Bug squashing day !Gravatar msozeau2008-04-17
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* Fixed bug 1761 (unexpected anomaly when constructor type has invalidGravatar herbelin2008-01-05
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...Gravatar herbelin2007-02-24
* Utilisation de l'environnement pour l'affichage de certains messages d'erreursGravatar herbelin2007-02-21
* Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentGravatar herbelin2007-01-24
* Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...Gravatar notin2006-10-05
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Messages nth brancheGravatar herbelin2006-02-07
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas laGravatar herbelin2006-01-30
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* 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
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Amélioration message d'erreur v8Gravatar herbelin2004-12-03
* Semble raisonnable de distinguer les noms aussi dans cant_applyGravatar herbelin2004-10-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Correction bug #830 : les noms des implicites temporaires étaient inconnus a...Gravatar herbelin2004-08-23
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #790: better error_not_cleanGravatar barras2004-07-13
* Traduction 'Cases' en pattern-matchingGravatar herbelin2004-02-28
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* Boite autour des quote pour eviter un retour a la ligne apres le premier guil...Gravatar herbelin2004-02-04
* Protection contre noms de variable indefinis et guillemets autour des constrGravatar herbelin2004-02-03
* Utilisation nom dans message d'erreur implicite pas trouveGravatar herbelin2003-11-29
* Amelioration message d'erreurGravatar herbelin2003-11-04
* message d'erreur de garde des cofixGravatar barras2003-09-22
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Restauration de make_all_different (disparu depuis version 1.74) car sinon de...Gravatar herbelin2003-03-31
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* *** empty log message ***Gravatar barras2003-03-12