coq - The formal proof system

Age	Commit message (Expand)	Author
2013-05-12	Use the Hook module here and there.	ppedrot
2013-05-09	Use definition_entry to declare local definitions	gareuselesinge
2013-05-09	Cosmetic change	gareuselesinge
2013-05-08	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot
2013-05-06	States: frozen states can hold closures	gareuselesinge
2013-05-06	Summary: support selective freeze	gareuselesinge
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-23	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey
2013-04-23	coqtop -compile: avoid with_heavy_rollback when non-interactive	letouzey
2013-04-22	code simplifications concerning Summary	letouzey
2013-04-22	Declaremods: some more minor cleanup	letouzey
2013-04-15	Minor simplifications in Declaremods and Safe_typing	letouzey
2013-04-15	Declaremods: drop some useless stuff (slight gain in vo size)	letouzey
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-03-28	Safe_typing+Libary: use some arrays instead of lists in vo structures	letouzey
2013-03-26	Synchronizing loadpath with the backtrack mechanism.	ppedrot
2013-03-26	Moved the Loadpath part of Library to its own file, and documented	ppedrot
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-21	Removing mandatory suffixes for library files.	ppedrot
2013-03-13	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey
2013-03-13	Declaremods: a few syntactic improvements	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 6)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey
2013-03-12	Restrict (try...with...) to avoid catching critical exn (part 1)	letouzey
2013-03-11	Added a Local Definition vernacular command. This type of definition	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-26	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey
2013-02-26	Mod_subst: misc reformulations	letouzey
2013-02-24	Reduced the noise level when dynlinking in bytecode mode or when	mdenes
2013-02-19	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-19	module_path --> ModPath.t, kernel_name --> KerName.t	letouzey
2013-02-19	Classops : avoid some use of Gmap	letouzey
2013-02-19	Names: revised representation of constants and mutual_inductive	letouzey
2013-02-18	use List.rev_map whenever possible	letouzey
2013-02-18	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey
2013-02-01	v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)	herbelin
2013-01-28	Fixed bug #2966 (de Bruijn error in computation of heads for coercions).	herbelin
2013-01-28	Actually adding backtrace handling.	ppedrot
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-27	Improving formatting of output of "Test table".	herbelin
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-12-18	Modulification of name	ppedrot
2012-12-18	Modulification of mod_bound_id	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Stringset and Stringmap to String namespace.	ppedrot