coq - The formal proof system

Age	Commit message (Expand)	Author
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
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-17	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-14	Fix extraction of inductive types that Coq auto-detects to be in Prop	letouzey
2013-02-13	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-12	Checker: re-sync vo structures after Maxime's commit 16136	letouzey
2013-02-11	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes
2013-02-10	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot
2013-02-10	Splitted Evarutil in two files	ppedrot
2013-02-10	Moved code from Pretype_error to Evarutil	ppedrot
2013-02-05	Revert "Ordered evars by level of dependency in the merging phase of unificat...	herbelin
2013-02-05	Fixed bug #2981 (anomaly NotASort in Retyping due to collision between	herbelin
2013-02-03	Fixing coqchk compilation after commit r16183	ppedrot