coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Term dnets do no need to contain the afferent constr pattern in their nodes.	Pierre-Marie Pédrot	2014-03-03
*	Removing Termdn, and putting the relevant code in Btermdn. The current Termdn	Pierre-Marie Pédrot	2014-03-03
*	Extruding code not depending of the functor argument in Termdn.	Pierre-Marie Pédrot	2014-03-03
*	Replacing arguments of Trie by a cancellable monoid.	Pierre-Marie Pédrot	2014-03-03
*	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot	2014-03-03
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Set officially the minimal OCaml requirement to 3.12.1	Pierre Letouzey	2014-03-02
*	Makefile: the initial build of grammar.cma is now directory-driven	Pierre Letouzey	2014-03-02
*	Migrate back g_obligations in toplevel	Pierre Letouzey	2014-03-02
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	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