aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* Adding printing of ltac envs to debugger.Gravatar Pierre-Marie Pédrot2013-11-30
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* A file listing old svn branches and tagsGravatar letouzey2013-11-18
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...Gravatar aspiwack2013-11-02
* Removes Refine from the dev tools now that the module has been deleted.Gravatar aspiwack2013-11-02
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* - install evar printer for debuggingGravatar msozeau2013-10-29
* Ephemeron: marshaling friendly keysGravatar gareuselesinge2013-10-18
* Adding evar printing to debugger.Gravatar ppedrot2013-09-24
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Fix compilation of dev/printres.cmaGravatar gareuselesinge2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Future library to represent pure computationsGravatar gareuselesinge2013-08-08
* Small cleaning of printing coercion failures in Ltac interpretation.Gravatar ppedrot2013-08-04
* Removing SortArgType.Gravatar ppedrot2013-07-05
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Adding genarg printer to debugger.Gravatar ppedrot2013-06-19
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Added Genarg as generic argument type.Gravatar ppedrot2013-06-12
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Adding a persistent stream data structure.Gravatar ppedrot2013-05-28
* Gmap is now useless, hail to Map!Gravatar ppedrot2013-05-14
* Removing useless uses of Gmap.Gravatar ppedrot2013-05-14
* Removing Fmap from libraries, it is not used anymore.Gravatar ppedrot2013-05-14
* Removing Fset, since it is not used anymore.Gravatar ppedrot2013-05-12
* Added a generic notion of hook. Hooks are functions to be setGravatar ppedrot2013-05-12
* Getting rid of module Gmapl.Gravatar ppedrot2013-05-09
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* add Loadpath to printers.mllibGravatar gareuselesinge2013-05-09
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Fix for bug #3017: wrong handling of the unresolvability statusGravatar msozeau2013-04-03
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
* Updated Exninfo to the new Store type.Gravatar ppedrot2013-03-12
* Update debug code according to reorganization into modules.Gravatar msozeau2013-02-27
* remove a warning after Drop about print_hint_dbGravatar letouzey2013-02-27
* Adapt dev/base_include to new DeclarationsGravatar letouzey2013-02-27
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Added Evarsolve to the list of modules to open for debugging.Gravatar herbelin2013-02-21
* Dir_path --> DirPathGravatar letouzey2013-02-19
* 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