coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extraction: qualified names in Extract Constant examples (fix #2878)	letouzey	2012-12-18
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Extraction of projections: restrict a hack to ocaml only (fix #2941)	letouzey	2012-12-17
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Stringset and Stringmap to String namespace.	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Ensure that a function declared with a label is used with it	letouzey	2012-12-08
*	Taking into account the type of a definition (if it exists), and the	herbelin	2012-11-17
*	More monomorphizations	ppedrot	2012-11-13
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	correcting a little bug in Function	jforest	2012-10-31
*	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-30
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	still some more dead code removal	letouzey	2012-10-06
*	remove useless hidden_flag in TacMutual(Co)Fix	letouzey	2012-10-06
*	remove dumptree.ml4	letouzey	2012-10-06
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06
*	Proof_type: rule now degenerates to prim_rule	letouzey	2012-10-06
*	Clean-up : no more Proof_type.proof_tree	letouzey	2012-10-06
*	Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box	letouzey	2012-10-06
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	Cleaning, renaming obscure functions and documenting in Hashcons.	ppedrot	2012-09-26
*	Fixing a bug introduced in Funind plugin when reorganizing the CList	ppedrot	2012-09-24
*	More cleaning in CArray...	ppedrot	2012-09-18
*	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey	2012-09-18
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Made Pp.std_ppcmds opaque.	ppedrot	2012-09-13
*	Fix Extraction Implicit on axioms.	aspiwack	2012-08-24
*	Experimental support for a comment in the files' preamble in extraction.	aspiwack	2012-08-24
*	Add option Set/Unset Extraction Conservative Types.	aspiwack	2012-08-24
*	Updating headers.	herbelin	2012-08-08
*	Fixup for macOS 10.8 & Ocaml 4.0	pboutill	2012-08-08
*	Vecnacentries.dump_global silently ignores exceptions	pboutill	2012-08-06
*	Try to make the use of Unix.lockf in micromega compatible with Win32	letouzey	2012-08-06
*	Dump references in Extraction	pboutill	2012-08-05
*	Dump references	pboutill	2012-08-05