coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Documentation of the "Local Definition" command.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	catch failures of pr_vernac to make -time failsafe	gareuselesinge	2013-03-08
*	Use with_state_protection in pr_module_vardecls	gareuselesinge	2013-03-08
*	More monomorphization.	ppedrot	2013-03-05
*	Missing primitive in CArray	ppedrot	2013-03-05
*	compare_stack_shape before ise_stack2 in evar_conv	pboutill	2013-02-28
*	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin	2013-02-28
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
*	Coqlib: minor simplifications	letouzey	2013-02-27
*	Update debug code according to reorganization into modules.	msozeau	2013-02-27
*	Minor cleanup around Term_typing	letouzey	2013-02-27
*	remove a warning after Drop about print_hint_db	letouzey	2013-02-27
*	Adapt dev/base_include to new Declarations	letouzey	2013-02-27
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Names: Modularize constant and mutual_inductive	letouzey	2013-02-26
*	Mod_subst: misc reformulations	letouzey	2013-02-26
*	cbn friendly VectorDef	pboutill	2013-02-25
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill	2013-02-25
*	CoqIDE: Add TAB key to autocomplete	ppedrot	2013-02-25
*	Fixing bug #2466	ppedrot	2013-02-24
*	New -no-native-compiler flag for configure, globally disabling the native	mdenes	2013-02-24
*	Reduced the noise level when dynlinking in bytecode mode or when	mdenes	2013-02-24
*	Tentative heuristic fix to handle lexer failures from CoqIDE when	ppedrot	2013-02-22
*	Cosmetic changes to CoqIDE finder widget.	ppedrot	2013-02-22
*	Names: con_modpath and con_label access back the user kn part	letouzey	2013-02-21
*	Added missing documentation of Set Printing Existential Instances.	herbelin	2013-02-21
*	A slightly more efficient test of well-typedness of restriction of	herbelin	2013-02-21
*	Added Evarsolve to the list of modules to open for debugging.	herbelin	2013-02-21
*	Fixing an annoying bug in CoqIDE which causes the very first line	ppedrot	2013-02-20
*	Fixing #2763	ppedrot	2013-02-20
*	More handling of scrollbars in CoqIDE completion	ppedrot	2013-02-20
*	CoqIDE: Including autocompletion in word proposals	ppedrot	2013-02-20
*	Corrects bug #2959 (error during Qed leads to assertion failure).	aspiwack	2013-02-20
*	Adding scrollbars to CoqIDE autocompletion	ppedrot	2013-02-20
*	New autocompletion mechanism in CoqIDE. Now provides many answers	ppedrot	2013-02-19
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19
*	module_path --> ModPath.t, kernel_name --> KerName.t	letouzey	2013-02-19
*	Mod_subst: an extra assert	letouzey	2013-02-19
*	Classops : avoid some use of Gmap	letouzey	2013-02-19
*	Names: revised representation of constants and mutual_inductive	letouzey	2013-02-19
*	Mod_subst: improve sharing during kn substitutions	letouzey	2013-02-18
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Adding more primitives to Exninfo	ppedrot	2013-02-18
*	Updating the backtrace handling mechanism to accomodate the new	ppedrot	2013-02-18
*	Added exception enrichment. Now one can define additional arbitrary	ppedrot	2013-02-18