coq - The formal proof system

Age	Commit message (Expand)	Author
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-11	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-08	catch failures of pr_vernac to make -time failsafe	gareuselesinge
2013-03-08	Use with_state_protection in pr_module_vardecls	gareuselesinge
2013-03-05	More monomorphization.	ppedrot
2013-03-05	Missing primitive in CArray	ppedrot
2013-02-28	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-27	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-26	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-25	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-24	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-22	Tentative heuristic fix to handle lexer failures from CoqIDE when	ppedrot
2013-02-22	Cosmetic changes to CoqIDE finder widget.	ppedrot
2013-02-21	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-20	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-19	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-18	Mod_subst: improve sharing during kn substitutions	letouzey
2013-02-18	Removing Exc_located and using the new exception enrichement	ppedrot