coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing generic equality in Syntax plugin.	Pierre-Marie Pédrot	2014-03-02
*	Adding an equality function over glob_constr	Pierre-Marie Pédrot	2014-03-02
*	Fixing generic Hashtbl.hash in Constr.	Pierre-Marie Pédrot	2014-03-02
*	Fix syntax highlighting of "Implicit Arguments" for gtksourceview.	Guillaume Melquiond	2014-03-02
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Better behaviour for sets of reserved names.	Pierre-Marie Pédrot	2014-03-01
*	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot	2014-03-01
*	Fixing bad comparison in Detyping.	Pierre-Marie Pédrot	2014-03-01
*	Useless check when loading notations through import.	Pierre-Marie Pédrot	2014-03-01
*	Hunting pervasive equality in native compiler. It seems they were used for	Pierre-Marie Pédrot	2014-03-01
*	Removing a fishy use of pervasive equality in Ltac backtrace printing.	Pierre-Marie Pédrot	2014-03-01
*	Removing Pervasives.compare in Termdn.	Pierre-Marie Pédrot	2014-02-28
*	Removing a Pervasives.compare in Term_dnet.	Pierre-Marie Pédrot	2014-02-28
*	Pos.compare_cont takes the comparison as first argument	Pierre Boutillier	2014-02-28
*	Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...	Pierre Boutillier	2014-02-28
*	test-suite: opaque term -> opaque proof	Pierre Boutillier	2014-02-28
*	test-suite: New names for vars but the expected invariant is preserved	Pierre Boutillier	2014-02-28
*	Fix output test-suite 'simpl tactic' -> 'reduction tactics'	Pierre Boutillier	2014-02-28
*	Dead code elimionation in reductionops	Pierre Boutillier	2014-02-28
*	.*.aux erased by make distclean	Pierre Boutillier	2014-02-28
*	Fix compilation of coq and plugins using coq_makefile under cygwin	Enrico Tassi	2014-02-28
*	Fixing a Pervasive.compare.	Pierre-Marie Pédrot	2014-02-28
*	Makefile: re-introduce 2 phases to avoid make strange -include's	Pierre Letouzey	2014-02-27
*	amending last commit	Enrico Tassi	2014-02-27
*	better warning	Enrico Tassi	2014-02-27
*	Tacinterp: more refactoring.	Arnaud Spiwack	2014-02-27
*	Tacinterp: refactoring using Monad.	Arnaud Spiwack	2014-02-27
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Get rid of the enterl/glist API for Proofview.Goal.	Arnaud Spiwack	2014-02-27
*	Tacinterp: yet another superfluous enterl.	Arnaud Spiwack	2014-02-27
*	Tacinterp: spurious enterl.	Arnaud Spiwack	2014-02-27
*	Dead code: eval_ltac_constr.	Arnaud Spiwack	2014-02-27
*	STM: better debug messages	Enrico Tassi	2014-02-26
*	STM: do not print goals on Undo	Enrico Tassi	2014-02-26
*	CoqIDE: print message of "Fail" command	Enrico Tassi	2014-02-26
*	refman: document vi2vo	Enrico Tassi	2014-02-26
*	STM: better messages when checking/finishing tasks	Enrico Tassi	2014-02-26
*	Library: when compiling multiple files, reset the opaque tables	Enrico Tassi	2014-02-26
*	STM: when batch compiling a vo, assert we behave conservatively	Enrico Tassi	2014-02-26
*	coq_makefile: new target vi2vo	Enrico Tassi	2014-02-26
*	vi2vo: new flag -schedule-vi2vo	Enrico Tassi	2014-02-26
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	STM: backup/restore remote counters	Enrico Tassi	2014-02-26
*	remoteCounter: backup/restore	Enrico Tassi	2014-02-26
*	univ: removing dead code	Enrico Tassi	2014-02-26
*	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	votour: better error messages	Enrico Tassi	2014-02-26