coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
*	Fix treatment of notations containing applications of projections (fixes bug ...	Matthieu Sozeau	2014-07-29
*	Continue fix on argument scopes of primitive projections.	Matthieu Sozeau	2014-06-17
*	Fixing #3282 (two bugs in the presence of let-in's in "fix").	Hugo Herbelin	2014-06-17
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	Fix bug #3289	Matthieu Sozeau	2014-06-11
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Fix printing of projections with implicits.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	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