coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fix a confusion between types of locations in an untyped part of the parser	letouzey	2012-10-05
*	Repair the configure after Hugo's last "repair" ;-)	letouzey	2012-10-05
*	coqtop -time : display per-command timings	letouzey	2012-10-05
*	More accurate timings for "Time foo"	letouzey	2012-10-05
*	Revert r15851 "En cours pour bug 2836".	herbelin	2012-10-04
*	Revert "En cours pour 'generalize in clause' et 'induction in clause'"	herbelin	2012-10-04
*	Repaired configure damaged in r15748 for those bash users which have	herbelin	2012-10-04
*	Suggest to use clean rather than archclean before recompiling.	herbelin	2012-10-04
*	Improving error message when abtraction over goal (abstract_list_all	herbelin	2012-10-04
*	En cours pour 'generalize in clause' et 'induction in clause'	herbelin	2012-10-04
*	En cours pour bug 2836	herbelin	2012-10-04
*	Makefile.build: easier compilation with timings info	letouzey	2012-10-04
*	Getting rid of Compat in the checker.	ppedrot	2012-10-04
*	Adding a nominal typing layer to Metasyntax in order to clarify	ppedrot	2012-10-04
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Remove the unused "intel" field in Proof.proof_state	letouzey	2012-10-02
*	Remove some dead code in the vm	letouzey	2012-10-02
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Argextend: avoid useless "open Extrawit"	letouzey	2012-10-02
*	avoid referring to Term in constrexpr.mli and glob_term.mli	letouzey	2012-10-02
*	New makefile shortcuts miniopt and minibyte for coqtop + plugins	letouzey	2012-10-02
*	Use the library function List.substract in prev commit	letouzey	2012-10-02
*	Added a new tactical infoH tac, that displays the names of hypothesis created...	courtieu	2012-10-01
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	Default hashconsing of identifiers.	ppedrot	2012-09-27
*	Reusing the Hashset data structure in Hashcons. Hopefully, this should	ppedrot	2012-09-26
*	Incorrect comment	msozeau	2012-09-26
*	Cleaning, renaming obscure functions and documenting in Hashcons.	ppedrot	2012-09-26
*	Fixing ocamldoc errors	ppedrot	2012-09-25
*	Added a ml-dot option to Makefile to generate dependency graph of core modules	ppedrot	2012-09-25
*	Fixing #2865.	ppedrot	2012-09-25
*	Fixing a bug introduced in Funind plugin when reorganizing the CList	ppedrot	2012-09-24
*	Fix use of $(HASNATDYNLINK) in coq_makefile output	glondu	2012-09-22
*	Avoid generating ide/coqide_main*.ml as cleartext (except if READABLE_ML4 is ...	letouzey	2012-09-20
*	Remove broken makefile option NO_RECOMPILE_LIB	letouzey	2012-09-20
*	Fixing Show Script issues.	ppedrot	2012-09-20
*	Coq_makefile fixups	pboutill	2012-09-18
*	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
*	MacOS integration uses lablgtkosx >= 1.1	pboutill	2012-09-17
*	More type-safe interface to Coq XML API.	ppedrot	2012-09-17
*	Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen...	gmelquio	2012-09-16
*	Some more fixes to tactic documentation.	gmelquio	2012-09-16
*	Beautify tactic documentation a bit more.	gmelquio	2012-09-16
*	Remove superfluous spaces and commas in tactic documentation.	gmelquio	2012-09-16