coq - The formal proof system

Age	Commit message (Expand)	Author
2013-06-24	Using the whole tactic environment while Pretyping.	ppedrot
2013-06-22	Generalizing the use of maps instead of lists in the interpretation	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-06	Fixing bug #3030.	ppedrot
2013-06-06	More comments in Genarg.	ppedrot
2013-06-06	Add an option to shrink the context of program obligations to avoid	msozeau
2013-06-05	Replacing lists by maps in matching interpretation.	ppedrot
2013-06-02	Making the behavior of "injection ... as ..." more natural:	herbelin
2013-05-30	Removing a useless location in ltac trace mechanism.	ppedrot
2013-05-28	Getting rid of LtacLocated exception transformer.	ppedrot
2013-05-14	Replacing Id.check with Id.is_valid, as its sole use was under	ppedrot
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	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