coq - The formal proof system

Age	Commit message (Expand)	Author
2013-05-09	Use definition_entry to declare local definitions	gareuselesinge
2013-05-09	Getting rid of module Gmapl.	ppedrot
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-05-09	Uniformization: isevars -> evdref/sigma/evd	herbelin
2013-05-09	Fixing r16487 on sharing evars between multiple parameters (missing List.rev).	herbelin
2013-05-08	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot
2013-05-08	Declaration of multiple hypotheses or parameters now share typing	herbelin
2013-05-08	Share more information between constructors and arity of an inductive	herbelin
2013-05-06	New module Xml_printer (dual to Xml_parser)	gareuselesinge
2013-05-06	States: frozen states can hold closures	gareuselesinge
2013-05-06	Close the .glob file after having saved .vo	gareuselesinge
2013-05-05	Improvement of r16204 on reporting tactic error locations: if the main	herbelin
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-25	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-23	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-22	code simplifications concerning Summary	letouzey
2013-04-19	interface.mli and serialize.ml reworked to avoid copy/paste of types	gareuselesinge
2013-04-18	Only arguments declared as implicit can be renamed	gareuselesinge
2013-04-17	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-15	More functional implementation of locality_flag and program_mode	gareuselesinge
2013-04-11	Backport r16394 from 8.4:	msozeau
2013-04-03	Fix for bug #3017: wrong handling of the unresolvability status	msozeau
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-04-02	Exporting the SearchAbout filter.	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-22	Fix bug# 2994, 2971 about better error messages.	msozeau
2013-03-21	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-19	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot
2013-03-18	Making local variable warning verbose by default.	ppedrot
2013-03-17	Avoid a few overzealous "when Errors.noncritical"	letouzey
2013-03-14	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-13	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