aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* Quick improvement of some error messages related to module applicationGravatar herbelin2011-08-30
* Improving error message about coinductive guard (old "cases" is now "match")Gravatar herbelin2011-08-10
* Fix nf_evars_undefined use in pr_constraintsGravatar msozeau2011-08-03
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
* Finish branching functions handling module errors (cf. r13886)Gravatar letouzey2011-03-16
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
* A few more betaiota on environments and types of error messages. Seems toGravatar herbelin2011-03-05
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Misc improvements about evar_mapGravatar letouzey2010-12-15
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Add information of localisation when an error involving an "implicitGravatar herbelin2010-11-07
* Two [Evd.fold] turned into [Evd.fold_undefined].Gravatar aspiwack2010-10-04
* Fixed a bug in printing fix/cofix error messages when severalGravatar herbelin2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 13:52:08 +0000