aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* Removing dependency of Himsg in tactic files.Gravatar Pierre-Marie Pédrot2016-03-06
* Moving Ltac traces to Tacexpr and Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \
| | * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ |/|
| * Improving error message with missing patterns in the presence ofGravatar Hugo Herbelin2016-02-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\|
| * Fixing bug #3826: "Incompatible module types" is uninformative.Gravatar Pierre-Marie Pédrot2016-01-24
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\|
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
| * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:12:23 +0000