aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* 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
* - Allow parsing of @const@{instance} for specifying universe instances of pol...Gravatar Matthieu Sozeau2014-06-04
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
* Do not print tactic notation names at each interpretation step.Gravatar ppedrot2013-11-12
* Moving potentially costly computation from exception raising to messageGravatar ppedrot2013-10-22
* Removing uses of Evar.add in class-related functions.Gravatar ppedrot2013-10-06
* Removing dubious use of evarmap manipulating functions in printingGravatar ppedrot2013-10-05
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 04:54:12 +0000