index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
...
*
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-07-02
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Adding genarg printer to debugger.
ppedrot
2013-06-19
*
Proof-of-concept: moved four easy-to-handle generic arguments to
ppedrot
2013-06-18
*
Added Genarg as generic argument type.
ppedrot
2013-06-12
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
Adding a persistent stream data structure.
ppedrot
2013-05-28
*
Gmap is now useless, hail to Map!
ppedrot
2013-05-14
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
*
Removing Fmap from libraries, it is not used anymore.
ppedrot
2013-05-14
*
Removing Fset, since it is not used anymore.
ppedrot
2013-05-12
*
Added a generic notion of hook. Hooks are functions to be set
ppedrot
2013-05-12
*
Getting rid of module Gmapl.
ppedrot
2013-05-09
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
add Loadpath to printers.mllib
gareuselesinge
2013-05-09
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Fix for bug #3017: wrong handling of the unresolvability status
msozeau
2013-04-03
*
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
letouzey
2013-03-21
*
Updated Exninfo to the new Store type.
ppedrot
2013-03-12
*
Update debug code according to reorganization into modules.
msozeau
2013-02-27
*
remove a warning after Drop about print_hint_db
letouzey
2013-02-27
*
Adapt dev/base_include to new Declarations
letouzey
2013-02-27
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Added Evarsolve to the list of modules to open for debugging.
herbelin
2013-02-21
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Added exception enrichment. Now one can define additional arbitrary
ppedrot
2013-02-18
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Splitted Evarutil in two files
ppedrot
2013-02-10
*
Added backtrace primitives.
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Revert "remove -rectypes except for term.ml"
mdenes
2013-01-22
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moving hcons_string to String namespace.
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Added a CString module.
ppedrot
2012-11-13
*
Added an Int module with dummy utility functions.
ppedrot
2012-11-08
*
Cleared a purely declarative .ml file and moved its interface to intf/
ppedrot
2012-10-23
*
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-10-16
*
Turn mltop.ml4 into a regular ocaml file
letouzey
2012-10-06
*
still some more dead code removal
letouzey
2012-10-06
*
remove -rectypes except for term.ml
letouzey
2012-10-06
*
Clean-up : no more Proof_type.proof_tree
letouzey
2012-10-06
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-04
*
Cleaning, renaming obscure functions and documenting in Hashcons.
ppedrot
2012-09-26
[prev]
[next]