coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nicer code concerning dirpaths and modpath around Lib	letouzey	2013-08-22
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Modulification and removing of structural equality in Stateid.	ppedrot	2013-08-19
*	Support Proof General	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Added a Print Debug GC command that displays the current state of	ppedrot	2013-08-01
*	Added printing of instance priority to the Print Instances command.	ppedrot	2013-08-01
*	Granting bug #3098: adding priority to Existing Instances.	ppedrot	2013-08-01
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Lib.contents () instead of Lib.contents_after None	letouzey	2013-07-17
*	More dynamic argument scopes	letouzey	2013-07-17
*	Added a Register Inline command for the native compiler. Will be ported to th...	mdenes	2013-07-10
*	Removing SortArgType.	ppedrot	2013-07-05
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05
*	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot	2013-07-02
*	Getting rid of IntroPatternArgType.	ppedrot	2013-06-27
*	Removing useless tactic arguments, and using generic arguments	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
*	Removing useless uses of Gmap.	ppedrot	2013-05-14
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Now printing body of abbreviations (i.e. notation with a name) with	herbelin	2013-05-05
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	Improving error message in explain_cannot_find_well_typed_abstraction:	herbelin	2013-04-17
*	More functional implementation of locality_flag and program_mode	gareuselesinge	2013-04-15
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Printmod: handle more examples thanks to better nametab use	letouzey	2013-03-21
*	Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)	letouzey	2013-03-21
*	Ppvernac: no globalization for printing ltac definitions	letouzey	2013-03-17
*	Pptactic.pr_raw_tactic is now without env argument	letouzey	2013-03-14
*	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 13)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey	2013-03-13
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	Use with_state_protection in pr_module_vardecls	gareuselesinge	2013-03-08
*	More monomorphization.	ppedrot	2013-03-05
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18