coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moved Entries module back to kernel	ppedrot	2012-10-26
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Removed a few calls to "Opaque" in Logic.v ineffective since at least	herbelin	2012-10-24
*	Cleared a purely declarative .ml file and moved its interface to intf/	ppedrot	2012-10-23
*	Coqmktop: missing -I (fix #2851)	letouzey	2012-10-23
*	the new .dir-locals.el thanks to Pierre Courtieu	pboutill	2012-10-23
*	Text inserted by insert_this_phrase_on_success correct tagging	pboutill	2012-10-23
*	Coqide for Gtk-mac-integration 2.0.0	pboutill	2012-10-23
*	RefMan-tac: fix a few glitches concerning the documentation of eqn:	letouzey	2012-10-23
*	Fix bug #2892	letouzey	2012-10-22
*	Coqide does not need dllcoqrun.so	pboutill	2012-10-22
*	Makefile.build: CONFIG is now in clib	pboutill	2012-10-17
*	Do not install libcoqrun.so if compiled with -custom	pboutill	2012-10-17
*	Cygwin gcc do not accept -mno-cygwin anymore	pboutill	2012-10-17
*	Fix test-suite output/* in bench	pboutill	2012-10-17
*	Taking into account that ocamlfind might find a package w/o the files	herbelin	2012-10-17
*	Using weak tables instead of plain hash tables while hashconsing.	ppedrot	2012-10-17
*	univ inconsistency error message gives evidence of a cycle	barras	2012-10-17
*	Removing redundant definition of case_eq (see #2919).	herbelin	2012-10-16
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.	herbelin	2012-10-16
*	Removed dead code about linking Module names in coqdoc.	herbelin	2012-10-16
*	Continue killing hidden tactics : no more generated h_xxx	letouzey	2012-10-15
*	Egramml: minor simplification	letouzey	2012-10-15
*	Stylistic improvement: avoid a "if match List.hd"	letouzey	2012-10-15
*	Coq_makefile: easier compilation with timings info (from r15850)	pboutill	2012-10-15
*	Makefiles: Only -I required dirs (config, lib, ide) when compiling coqide	pboutill	2012-10-15
*	Makefile.build: $(MLINCLUDES) out of $(OPT/BYTEFLAGS)	pboutill	2012-10-15
*	Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 int...	pboutill	2012-10-15
*	When loading a plugin, prefer .cma to .cmo	gareuselesinge	2012-10-14
*	fix r15860 : no slash after $(COQLIB)	letouzey	2012-10-08
*	restore compatibility with camlp5 < 6.00	letouzey	2012-10-06
*	Coqmktop: a misplaced Filename.quote prevented temp file cleanup	letouzey	2012-10-06
*	Turn mltop.ml4 into a regular ocaml file	letouzey	2012-10-06
*	ocamlbuild simplifications	letouzey	2012-10-06
*	Minor fix in the ./build wrapper for ocamlbuild	letouzey	2012-10-06
*	no need for camlp4 cma's in coq misc tools	letouzey	2012-10-06
*	still some more dead code removal	letouzey	2012-10-06
*	remove useless hidden_flag in TacMutual(Co)Fix	letouzey	2012-10-06
*	cosmetic concerning interp of TacShowHyps	letouzey	2012-10-06
*	remove Refiner.abstract_tactic and similar	letouzey	2012-10-06
*	remove -rectypes except for term.ml	letouzey	2012-10-06
*	remove dumptree.ml4	letouzey	2012-10-06
*	Adapt pieces of code needing -rectypes	letouzey	2012-10-06
*	avoid using rectypes in dnet.ml	letouzey	2012-10-06
*	avoid using rectypes in nametab.ml	letouzey	2012-10-06
*	Tacexpr: revised version that doesn't need -rectypes	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