coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Fixing interpretation of tactics in terms. It was forgetting part of the	Pierre-Marie Pédrot	2014-03-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Fix grammatical mistake in error message (bug #3238)	xclerc	2014-02-24
*	Fixing an interpretation bug with tactics in notations. For some obscure	Pierre-Marie Pédrot	2014-01-19
*	Disable GlobRef feedback (CoqIDE does nothing with them)	Enrico Tassi	2014-01-05
*	Notation variables are now taken into account as possible ltac bound variables	Pierre-Marie Pédrot	2013-12-22
*	Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at	Pierre-Marie Pédrot	2013-12-22
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Fixing bug #3165.	Pierre-Marie Pédrot	2013-11-23
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	Support Proof General	gareuselesinge	2013-08-08
*	Removing association lists in Constrintern.	ppedrot	2013-08-07
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	Useless use of maps in constr internalizing.	ppedrot	2013-06-25
*	Using the whole tactic environment while Pretyping.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot	2013-05-08
*	Alert when using ".." outside a Notation command.	herbelin	2013-05-08
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Coqide: Globalization feedback (proof of concept)	gareuselesinge	2013-04-25
*	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot	2013-03-19
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 3)	letouzey	2013-03-12
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fix bug 2958: Inductive deep in in clause are impossible	pboutill	2013-01-21
*	Modulification of name	ppedrot	2012-12-18
*	Fixed interpretation of "x" as a binding variable for the return	herbelin	2012-12-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot	2012-12-14
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Backtrack on activating scopes with type casts (was r15978).	herbelin	2012-12-04
*	Monomorphization (interp)	ppedrot	2012-11-25
*	More equality functions	ppedrot	2012-11-25
*	Taking into account the type of a definition (if it exists), and the	herbelin	2012-11-17
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	As r15801: putting everything from Util.array_* to CArray.*.	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