coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Unifying locate code, also making it more powerful: it is now able to find	Pierre-Marie Pédrot	2014-07-21
*	Adding a new "Locate Term" command, distinct from the raw "Locate" command.	Pierre-Marie Pédrot	2014-07-21
*	More complete printing of Ltac location, akin to the term-dedicated Locate co...	Pierre-Marie Pédrot	2014-07-21
*	smartlocate: look for the head symbol for real	Enrico Tassi	2014-07-14
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
*	Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.	Matthieu Sozeau	2014-06-23
*	- Add "Show Universes" to print information about universes during a proof.	Matthieu Sozeau	2014-06-16
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	Adding a toplevel option allowing to deactivate the term sharing in kernel	Pierre-Marie Pédrot	2014-06-08
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	Remove the syntax [Vernac1. Vernac2. … Vernacn. ].	Arnaud Spiwack	2014-06-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	- Fix handling of polymorphic inductive elimination schemes.	Matthieu Sozeau	2014-05-06
*	- Fix Check to use the constraints inferred during type inference.	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25
*	Fixing various backtrace recordings.	Pierre-Marie Pédrot	2014-04-25
*	Add an option -Q (tentative name).	Guillaume Melquiond	2014-04-08
*	Adding a Print Strategy vernacular command. It allows to check the	Pierre-Marie Pédrot	2014-03-19
*	Using Hashmaps by default in constant and inductive maps. This changes fold and	Pierre-Marie Pédrot	2014-03-07
*	Using HMaps in Safe_env.environments, hopefully improving performances.	Pierre-Marie Pédrot	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	CoqIDE: print message of "Fail" command	Enrico Tassi	2014-02-26
*	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier	2014-02-24
*	Timeout and Set Default Timeout fixed (closes: #3229)	Enrico Tassi	2014-02-10
*	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot	2014-02-02
*	Load implemented in CoqIDE/STM (closes: #3223)	Enrico Tassi	2014-01-30
*	Make Require verbose	Pierre Boutillier	2014-01-13
*	Proof_using: new syntax + suggestion	Enrico Tassi	2014-01-05
*	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
*	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack	2013-12-04
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
*	Made multiple-goal tactic work after all: .	aspiwack	2013-11-02
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23