aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* Added exception enrichment. Now one can define additional arbitraryGravatar ppedrot2013-02-18
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
* Added backtrace primitives.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Revert "remove -rectypes except for term.ml"Gravatar mdenes2013-01-22
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Added a CString module.Gravatar ppedrot2012-11-13
* Added an Int module with dummy utility functions.Gravatar ppedrot2012-11-08
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* Turn mltop.ml4 into a regular ocaml fileGravatar letouzey2012-10-06
* still some more dead code removalGravatar letouzey2012-10-06
* remove -rectypes except for term.mlGravatar letouzey2012-10-06
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* Remove broken makefile option NO_RECOMPILE_LIBGravatar letouzey2012-09-20
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* No need anymore to refer to COQLIB in ocamldebug-coqGravatar letouzey2012-08-23
* Updating headers.Gravatar herbelin2012-08-08
* Revert "Fixing include printers"Gravatar pboutill2012-08-05
* Fixing include printersGravatar ppedrot2012-08-03
* Bigint: avoid dependency over PpGravatar letouzey2012-07-30
* Severe reorganisation of the code of tactics in Proofview.Gravatar aspiwack2012-07-11
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* Some documentation of recent changes concerning interfacesGravatar letouzey2012-05-29
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
* Extend become a mli-only file in intf/Gravatar letouzey2012-05-29
* Split Egrammar into Egramml and EgramcoqGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Strongly reduce the dependencies of grammar.cma, modulo two hacksGravatar letouzey2012-05-29
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
* Coqide MacOS integration refreshGravatar pboutill2012-04-27
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* Removing Dhyp from debugger.Gravatar herbelin2012-04-06