coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Restrict (try...with...) to avoid catching critical exn (part 4)	letouzey	2013-03-12
*	Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...	letouzey	2013-03-12
*	Restrict (try...with...) to avoid catching critical exn (part 3)	letouzey	2013-03-12
*	Restrict (try...with...) to avoid catching critical exn (part 2)	letouzey	2013-03-12
*	Restrict (try...with...) to avoid catching critical exn (part 1)	letouzey	2013-03-12
*	Hipattern : consider jmeq only when Logic.JMeq is loaded	letouzey	2013-03-12
*	A version of Univ.check_eq with no anomaly for Evd.set_eq_sort	letouzey	2013-03-12
*	Equality: avoid an anomaly about inj_pair2_eq_dec	letouzey	2013-03-12
*	Recdef: an anomaly isn't so anomalous, occurs in 1618.v	letouzey	2013-03-12
*	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey	2013-03-12
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	New function Errors.noncritical for restricting try ... with ...	letouzey	2013-03-12
*	Updated Exninfo to the new Store type.	ppedrot	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
*	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