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
*
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
*
Remove broken makefile option NO_RECOMPILE_LIB
letouzey
2012-09-20
*
More cleanup of Util: utf8 aspects moved to a new file unicode.ml
letouzey
2012-09-18
*
Cleaning interface of Util.
ppedrot
2012-09-18
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
No need anymore to refer to COQLIB in ocamldebug-coq
letouzey
2012-08-23
*
Updating headers.
herbelin
2012-08-08
*
Revert "Fixing include printers"
pboutill
2012-08-05
*
Fixing include printers
ppedrot
2012-08-03
*
Bigint: avoid dependency over Pp
letouzey
2012-07-30
*
Severe reorganisation of the code of tactics in Proofview.
aspiwack
2012-07-11
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
Some documentation of recent changes concerning interfaces
letouzey
2012-05-29
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29
*
Extend become a mli-only file in intf/
letouzey
2012-05-29
*
Split Egrammar into Egramml and Egramcoq
letouzey
2012-05-29
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
[next]