aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* 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
* Himsg : strict 80-column indentationGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* Added more flags choice in desambiguating printer. The code isGravatar ppedrot2013-08-06
* Tentative fix for bug #2961. When we have to print two terms thatGravatar ppedrot2013-08-05
* Fixing #2846: Uncaught exception Reduction.NotArity.Gravatar ppedrot2013-08-04
* Using the whole tactic environment while Pretyping.Gravatar ppedrot2013-06-24
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* Replacing lists by maps in matching interpretation.Gravatar ppedrot2013-06-05
* Improvement of r16204 on reporting tactic error locations: if the mainGravatar herbelin2013-05-05
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Improving error message in explain_cannot_find_well_typed_abstraction:Gravatar herbelin2013-04-17
* Fix for bug #3017: wrong handling of the unresolvability statusGravatar msozeau2013-04-03
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
* Add type information in error message when a constructor is not fullyGravatar herbelin2013-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 09:45:57 +0000