aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Inductive parameters: nicer doc examples and error messageGravatar letouzey2008-11-28
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* Raise informative errors instead of Failures or anomalies in case a metaGravatar msozeau2008-10-24
* Fix bug #1940: uncaught exception when searching for a type class.Gravatar msozeau2008-09-14
* Various fixes w.r.t typeclasses and subtac: resolve tcs properly insideGravatar msozeau2008-08-21
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecGravatar herbelin2008-07-26
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* 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