aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
2013-03-12Updated Exninfo to the new Store type.ppedrot
2013-02-27Update debug code according to reorganization into modules.msozeau
2013-02-27remove a warning after Drop about print_hint_dbletouzey
2013-02-27Adapt dev/base_include to new Declarationsletouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-21Added Evarsolve to the list of modules to open for debugging.herbelin
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-10Splitted Evarutil in two filesppedrot
2013-01-28Added backtrace primitives.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2013-01-22Revert "remove -rectypes except for term.ml"mdenes
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Added an Int module with dummy utility functions.ppedrot
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-06Turn mltop.ml4 into a regular ocaml fileletouzey
2012-10-06still some more dead code removalletouzey
2012-10-06remove -rectypes except for term.mlletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-20Remove broken makefile option NO_RECOMPILE_LIBletouzey
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-23No need anymore to refer to COQLIB in ocamldebug-coqletouzey
2012-08-08Updating headers.herbelin
2012-08-05Revert "Fixing include printers"pboutill
2012-08-03Fixing include printersppedrot
2012-07-30Bigint: avoid dependency over Ppletouzey
2012-07-11Severe reorganisation of the code of tactics in Proofview.aspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-05-29Some documentation of recent changes concerning interfacesletouzey
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29Extend become a mli-only file in intf/letouzey
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Strongly reduce the dependencies of grammar.cma, modulo two hacksletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 01:54:38 +0000