aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* A hack to fix another regression with Ltac trace report in 8.5. E.g.Gravatar Hugo Herbelin2016-06-18
* Reserve exception "ConversionFailed" in unification for failure ofGravatar Hugo Herbelin2016-06-12
* Fixing bug in printing CannotSolveConstraint (collision of context names).Gravatar Hugo Herbelin2016-06-12
* Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
* Improving error message with missing patterns in the presence ofGravatar Hugo Herbelin2016-02-08
* Fixing bug #3826: "Incompatible module types" is uninformative.Gravatar Pierre-Marie Pédrot2016-01-24
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* Minor module cleanup : error HigherOrderInclude was never happeningGravatar Pierre Letouzey2015-10-25
* Fixing bug #4367: Wrong error message in unification.Gravatar Pierre-Marie Pédrot2015-10-14
* Also there's an extra space in the error message.Gravatar mlasson2015-09-03
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Better error message for nested module application.Gravatar Maxime Dénès2015-02-13
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding a redundant information in unification error message.Gravatar Hugo Herbelin2015-01-11
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
* Improving error message when one instance-hole is not found.Gravatar Hugo Herbelin2014-12-04
* Slight improving of a unification error message.Gravatar Hugo Herbelin2014-12-03
* Removing superfluous newlines in setoid_rewrite error message.Gravatar Hugo Herbelin2014-11-22
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Continuing 3741c46fe134 on reporting ltac error.Gravatar Hugo Herbelin2014-11-08
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Print type and environment of unsolved holes.Gravatar Arnaud Spiwack2014-10-02
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
* Fixing bug #3646.Gravatar Pierre-Marie Pédrot2014-09-19
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
* More explicit printing in Himsg.Gravatar Pierre-Marie Pédrot2014-09-04
* Print error messages with more hidden information based on α-equivalence .Gravatar Arnaud Spiwack2014-09-03
* Fixing bug #3533.Gravatar Pierre-Marie Pédrot2014-08-23
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Refined guard condition of cofixpoints, to anticipate potential futurGravatar Maxime Dénès2014-07-22
* First attempt at a fix for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* Fix spacing in error message.Gravatar Guillaume Melquiond2014-06-16
* Improved error message when a meta posed as an evar remains unsolvedGravatar Hugo Herbelin2014-06-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 22:55:49 +0000