coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Bigint: new functions of_int and to_int, 2nd arg of pow in int	letouzey	2012-08-02
*	Getting rid of the undocumented [complete] tactic, which was	ppedrot	2012-07-19
*	Fixes r15610 (A new status Unsafe in Interface).	aspiwack	2012-07-13
*	Ring_polynom : a restricted simpl instead of a unfold;fold	letouzey	2012-07-07
*	Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)	letouzey	2012-07-05
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite	letouzey	2012-07-05
*	More cleanup in Ring_polynom and EnvRing	letouzey	2012-07-05
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Cleaning opening of the standard List module.	ppedrot	2012-06-28
*	Replace nat indices with positive one in Btauto.	ppedrot	2012-06-28
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
*	More cleaning	ppedrot	2012-06-01