aboutsummaryrefslogtreecommitdiff
path: root/toplevel/himsg.ml
AgeCommit message (Expand)Author
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
2013-02-17Displaying environment and unfolding aliases in "cannot_unify"herbelin
2013-02-17A more informative message when the elimination predicate forherbelin
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2013-02-10Moved code from Pretype_error to Evarutilppedrot
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-04Improving error message when abtraction over goal (abstract_list_allherbelin
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-07-11Fix typeclass error handling which was sometimes raising a Failure ("hd").msozeau
2012-07-05rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 18:14:06 +0000