aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2013-08-08State Transaction Machinegareuselesinge
2013-08-08Future library to represent pure computationsgareuselesinge
2013-08-04Small cleaning of printing coercion failures in Ltac interpretation.ppedrot
2013-07-05Removing SortArgType.ppedrot
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-06-27Getting rid of IntroPatternArgType.ppedrot
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-19Adding genarg printer to debugger.ppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-06-12Added Genarg as generic argument type.ppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-05-28Adding a persistent stream data structure.ppedrot
2013-05-14Gmap is now useless, hail to Map!ppedrot
2013-05-14Removing useless uses of Gmap.ppedrot
2013-05-14Removing Fmap from libraries, it is not used anymore.ppedrot
2013-05-12Removing Fset, since it is not used anymore.ppedrot
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
2013-05-09Getting rid of module Gmapl.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-09add Loadpath to printers.mllibgareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:53:40 +0000