aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
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
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29Tacexpr as a mli-only, the few functions there are now in Tacopsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-04-27Coqide MacOS integration refreshpboutill
2012-04-12lib directory is cut in 2 cma.pboutill
2012-04-06Removing Dhyp from debugger.herbelin
2012-03-14Everything compiles again.msozeau
2012-03-02Noise for nothingpboutill
2012-02-01Debugger vs tracer: Two different behaviors wrt printing: The debuggerherbelin
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
2011-12-18Suspending declaration of undefined debug printers.herbelin
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-17Revert "New evar_map printer ppevmfull which can typically be installed for"herbelin
2011-10-17New evar_map printer ppevmfull which can typically be installed forherbelin
2011-10-15dev/base_include: display a nice message at the end of the loadletouzey
2011-10-15debugging.txt: no more typing of #use "include" if using .ocamlinitletouzey