aboutsummaryrefslogtreecommitdiff
path: root/toplevel/himsg.ml
AgeCommit message (Expand)Author
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-10Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Hugo Herbelin
2014-09-04More explicit printing in Himsg.Pierre-Marie Pédrot
2014-09-03Print error messages with more hidden information based on α-equivalence .Arnaud Spiwack
2014-08-23Fixing bug #3533.Pierre-Marie Pédrot
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-08-18Moving the TacAlias node out of atomic tactics.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-13Bettre pretty-printing of evar maps, avoids printing universe informationMatthieu Sozeau
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-07-22Refined guard condition of cofixpoints, to anticipate potential futurMaxime Dénès
2014-07-22First attempt at a fix for guard condition on cofixpoints.Maxime Dénès
2014-06-28Moved code for finding subterms (pattern, induction, set, generalize, ...)Hugo Herbelin
2014-06-28Made the subterm finding function make_abstraction independent of theHugo Herbelin
2014-06-16Fix spacing in error message.Guillaume Melquiond
2014-06-13Improved error message when a meta posed as an evar remains unsolvedHugo Herbelin
2014-06-04- Allow parsing of @const@{instance} for specifying universe instances of pol...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-01Removing a fishy use of pervasive equality in Ltac backtrace printing.Pierre-Marie Pédrot
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
2013-10-22Moving potentially costly computation from exception raising to messageppedrot
2013-10-06Removing uses of Evar.add in class-related functions.ppedrot
2013-10-05Removing dubious use of evarmap manipulating functions in printingppedrot
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Himsg : strict 80-column indentationletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-06Added more flags choice in desambiguating printer. The code isppedrot
2013-08-05Tentative fix for bug #2961. When we have to print two terms thatppedrot
2013-08-04Fixing #2846: Uncaught exception Reduction.NotArity.ppedrot
2013-06-24Using the whole tactic environment while Pretyping.ppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-05-05Improvement of r16204 on reporting tactic error locations: if the mainherbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-17Improving error message in explain_cannot_find_well_typed_abstraction:herbelin
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
2013-03-21Add type information in error message when a constructor is not fullyherbelin
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-05More monomorphization.ppedrot
2013-02-28Repairing r16205: errors raised by check_evar_instance were no longerherbelin
2013-02-28More informative error when a global reference is used in a context ofherbelin
2013-02-24Fixing bug #2466ppedrot
2013-02-18use List.rev_map whenever possibleletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 05:02:44 +0000