coq - The formal proof system

Age	Commit message (Expand)	Author
2012-12-07	Coqide: opening non-existing files won't create them immediately anymore	letouzey
2012-12-07	Coqide: nicer creation of timers	letouzey
2012-12-07	Coqide: code cleanup	letouzey
2012-12-07	* lib/Envars:	regisgia
2012-12-07	* lib/Envars:	regisgia
2012-12-07	Revert "* tools/Coq_makefile:"	regisgia
2012-12-07	* tools/Coq_makefile	regisgia
2012-12-07	* tools/Coq_makefile:	regisgia
2012-12-06	Restoring flush of Welcome message lost in r15148	herbelin
2012-12-05	Making subset_eq_compat applying over more general domain "Type" (see #2938).	herbelin
2012-12-04	Backtrack on activating scopes with type casts (was r15978).	herbelin
2012-12-04	Removed Compat.Exc_located outside of compat.ml4, as a consequence of	herbelin
2012-12-04	Early translation of camlp4/camlp5 located errors into coq-located	herbelin
2012-12-04	Low-level hack to get some more informative message from dynamic loading errors.	herbelin
2012-12-04	Fixing a comment.	herbelin
2012-12-04	Revised the strategy for automatic insertion of spaces when printing	herbelin
2012-12-04	Display Menu now called View Menu (in CoqIDE preferences).	herbelin
2012-12-04	Identities over types satisfying Uniqueness of Identity Proofs	herbelin
2012-12-04	Coqmktop: use the atomic Filename.open_temp_file	letouzey
2012-11-28	Evarconv: Fix #2936 + comments	pboutill
2012-11-28	Fix ocamldebug constr printer	pboutill
2012-11-28	Reductionops uses Closure.reds	pboutill
2012-11-28	Kernel/closure: add eta red_kind	pboutill
2012-11-26	Removed some FIXME related to equality on universes.	ppedrot
2012-11-26	Small cleaning of interface in Univ	ppedrot
2012-11-26	Monomorphization (toplevel)	ppedrot
2012-11-26	Fixed a monomorphization error.	ppedrot
2012-11-25	Monomorphization (tactics)	ppedrot
2012-11-25	Monomorphization (proof)	ppedrot
2012-11-25	Monomorphization (library)	ppedrot
2012-11-25	Monomorphization (parsing)	ppedrot
2012-11-25	Monomorphization (interp)	ppedrot
2012-11-25	More equality functions	ppedrot
2012-11-25	Fixed bug #2930: folded let-in's were hiding a violation to the occur	herbelin
2012-11-23	Added a constr_pattern_eq	ppedrot
2012-11-22	Monomorphization (pretyping)	ppedrot
2012-11-22	Monomorphization (library)	ppedrot
2012-11-22	Monomorphization (kernel)	ppedrot
2012-11-22	Monomorphization (lib)	ppedrot
2012-11-21	Fixing test-suite: Scope.v	ppedrot
2012-11-21	Print univ constraints generated by a constant or inductive (when flag is set)	barras
2012-11-20	Cleaning and small optimization in CList.	ppedrot
2012-11-19	Serialize: no need anymore to export of_value / to_value in the mli	letouzey
2012-11-19	Serialize: dead code	letouzey
2012-11-19	Serialize: fix dyn-typing of GetOptions (oups), also adapt of_answer	letouzey
2012-11-19	Serialize.to_answer: dynamically check that answer & call correspond	letouzey
2012-11-18	Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)	herbelin
2012-11-17	Update output/Search.out after hint-related extra defs in Peano	letouzey
2012-11-17	Print Assumptions: restore a final \n	letouzey
2012-11-17	Taking into account the type of a definition (if it exists), and the	herbelin