coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Extraction: same as commit 16203, hopefully without NotASort exns	letouzey	2013-02-18
*	Displaying environment and unfolding aliases in "cannot_unify"	herbelin	2013-02-17
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Locating errors from consider_remaining_unif_problems if possible	herbelin	2013-02-17
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Fix extraction of inductive types that Coq auto-detects to be in Prop	letouzey	2013-02-14
*	CoqIDE: Adding escape reaction to replace widget	ppedrot	2013-02-13
*	Fixing autocompletion lock in CoqIDE	ppedrot	2013-02-13
*	make validate repaired via a temporary fix for #2949	letouzey	2013-02-13
*	Checker: re-sync vo structures after Maxime's commit 16136	letouzey	2013-02-12
*	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes	2013-02-11
*	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot	2013-02-10
*	Splitted Evarutil in two files	ppedrot	2013-02-10