coq - The formal proof system

Age	Commit message (Expand)	Author
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
2012-11-15	Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing	herbelin
2012-11-15	Some lemmas on property of rewriting. It will probably be worth at	herbelin
2012-11-15	backtrack too much commited files in the last commit.	courtieu
2012-11-15	Fixing emacs diff bug with .dir-locals.el.	courtieu
2012-11-15	Added a proof that Prop<>Type, for arbitrary fixed Type.	herbelin
2012-11-15	A decidability property of functional relations over decidable codomains.	herbelin
2012-11-15	For the record, two examples of short proofs of uniqueness of identity	herbelin
2012-11-13	Small uniformization in String	ppedrot
2012-11-13	More monomorphizations	ppedrot
2012-11-13	Added a CString module.	ppedrot
2012-11-13	coq_makefile: use coqdep instead of ocamldep on .ml4 files	gareuselesinge
2012-11-13	Another GC test	ppedrot
2012-11-12	Add an option -nodoc to configure, same (but shorter) than -with-doc no	letouzey
2012-11-12	Coqide : allow properly closing communication pipes with coqtop	letouzey
2012-11-12	Ide_slave: do not attempt to answer broken requests	letouzey
2012-11-12	Xml_parser: detect immediate EOF + disable check_eof by default	letouzey
2012-11-12	Removed the modification of the GC pressure coefficient, in order	ppedrot
2012-11-08	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot
2012-11-08	Added an Int module with dummy utility functions.	ppedrot
2012-11-08	Removing another bunch of generic equalities	ppedrot
2012-11-07	Fix reference_or_constr grammar rule to accept @t as a constr	gareuselesinge
2012-11-06	Coq is a heavy user of persistent data structures and symbolic ASTs, so the	ppedrot
2012-11-03	Reversed roles of undefined/defined evars in Evd, thus saving precious	ppedrot
2012-10-31	Coqide Detach View: avoid doing gtk stuff in sub-thread (fix #2863)	letouzey
2012-10-31	Change [Hints Resolve] to still accept constrs as arguments	msozeau
2012-10-31	correcting a little bug in Function	jforest
2012-10-30	Documenting the 'Printing Transparent/All Dependencies' command.	ppedrot
2012-10-30	Extraction Implicit: consider the parameters of a constructor (fix #2905)	letouzey
2012-10-30	Extraction: avoid initial strange empty comments after Arnaud's hack	letouzey