| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-10-30 | Fix Separate extraction when a module-as-file is aliased (#2917) | letouzey |
| 2012-10-29 | coqdep: honor dependencies of "Load"ed files | gareuselesinge |
| 2012-10-29 | Allow running coq-tex in win32 (fix #2921) | letouzey |
| 2012-10-29 | Fixed #2926: | ppedrot |
| 2012-10-29 | Removed many calls to OCaml generic equality. This was done by | ppedrot |
| 2012-10-26 | Moved Entries module back to kernel | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-24 | Removed a few calls to "Opaque" in Logic.v ineffective since at least | herbelin |
| 2012-10-23 | Cleared a purely declarative .ml file and moved its interface to intf/ | ppedrot |
| 2012-10-23 | Coqmktop: missing -I (fix #2851) | letouzey |
