coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Declaremods: major refactoring, stop duplicating libobjects in modules	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 the use of leveled tactics wit_tacticn. It is now handled	ppedrot	2013-07-02
*	Using the whole tactic environment while Pretyping.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	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-06
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	Making the behavior of "injection ... as ..." more natural:	herbelin	2013-06-02
*	Removing a useless location in ltac trace mechanism.	ppedrot	2013-05-30
*	Getting rid of LtacLocated exception transformer.	ppedrot	2013-05-28
*	Replacing Id.check with Id.is_valid, as its sole use was under	ppedrot	2013-05-14
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	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-09
*	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-08
*	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-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