aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* missing space in error messageGravatar vsiles2010-04-20
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Hopefully improved layout of fix guardness error message.Gravatar herbelin2009-10-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Backport from v8.2 branch of 11986 (interpretation of quantifiedGravatar herbelin2009-03-22
* 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