coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Close the .glob file after having saved .vo	gareuselesinge	2013-05-06
*	Improvement of r16204 on reporting tactic error locations: if the main	herbelin	2013-05-05
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Fix compilation (vernac.ml, missing ;)	gareuselesinge	2013-04-25
*	Flag ide_slave moved into Flags module	gareuselesinge	2013-04-25
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
*	Coqide: new feedback mechanism for structured content	gareuselesinge	2013-04-25
*	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey	2013-04-23
*	minor cleanup in coqtop.ml	letouzey	2013-04-23
*	coqtop -compile: avoid with_heavy_rollback when non-interactive	letouzey	2013-04-23
*	Coqtop -compile : avoid saving init state when compiling just one file	letouzey	2013-04-23
*	Remove deprecated option -no-hash-consing (currently doing nothing)	letouzey	2013-04-23
*	code simplifications concerning Summary	letouzey	2013-04-22
*	interface.mli and serialize.ml reworked to avoid copy/paste of types	gareuselesinge	2013-04-19
*	Only arguments declared as implicit can be renamed	gareuselesinge	2013-04-18
*	Matching patterns: fixed allow_partial_app which was not working on	herbelin	2013-04-17
*	Coqc: repair localisation of errors in files	letouzey	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
*	Backport r16394 from 8.4:	msozeau	2013-04-11
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Exporting the SearchAbout filter.	ppedrot	2013-04-02
*	Moved the Loadpath part of Library to its own file, and documented	ppedrot	2013-03-26
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Fix bug# 2994, 2971 about better error messages.	msozeau	2013-03-22
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Typo dans message d'erreur (obligations).	herbelin	2013-03-21
*	Add type information in error message when a constructor is not fully	herbelin	2013-03-21
*	Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)	letouzey	2013-03-21
*	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot	2013-03-19
*	Making local variable warning verbose by default.	ppedrot	2013-03-18
*	Avoid a few overzealous "when Errors.noncritical"	letouzey	2013-03-17
*	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey	2013-03-14
*	Cerrors: get rid of some FIXME	letouzey	2013-03-14
*	Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)	letouzey	2013-03-14
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Toplevel: improved comments	letouzey	2013-03-13
*	Vernac+Toplevel: get rid of Error_in_file	letouzey	2013-03-13
*	Vernac+Toplevel: get rid of DuringVernacInterp	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 14)	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 10)	letouzey	2013-03-13
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Obligations generated by Program are now local.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11