coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot	2014-04-23
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Closing bug #3260	Julien Forest	2014-04-14
*	Removing the Change_evar refiner rule.	Pierre-Marie Pédrot	2014-03-31
*	Adding a Print Strategy vernacular command. It allows to check the	Pierre-Marie Pédrot	2014-03-19
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Fix output test-suite 'simpl tactic' -> 'reduction tactics'	Pierre Boutillier	2014-02-28
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier	2014-02-24
*	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot	2014-02-02
*	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot	2014-01-19
*	Follow-up of bugfix for #3204: local definitions were not handled properly.	Pierre-Marie Pédrot	2014-01-17
*	Fixing bugs #1039: Hypotheses don't respect Barendregt convention	Pierre-Marie Pédrot	2014-01-16
*	Proof_using: new syntax + suggestion	Enrico Tassi	2014-01-05
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	Printing function for Stdargs in debugger	Pierre Boutillier	2013-12-19
*	A few fixes to the build system (mostly for ocamlbuild)	Pierre Letouzey	2013-12-16
*	Removing RefArgType generic argument.	Pierre-Marie Pédrot	2013-12-01
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Synchronizing the printer of tactic notations.	ppedrot	2013-11-13
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	Update comments.	aspiwack	2013-11-02
*	Adds a tactic give_up.	aspiwack	2013-11-02
*	Adds a shelve tactic.	aspiwack	2013-11-02
*	Adds an experimental exactly_once tactical.	aspiwack	2013-11-02
*	Adds a tactical once.	aspiwack	2013-11-02
*	Added the tactical "tac1 + tac2".	aspiwack	2013-11-02
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	New option Default Goal Selector.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot	2013-10-27
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	STM: add "Stm Wait" to wait for the slaves to complete their jobs	gareuselesinge	2013-10-10
*	STM: new command "Stm PrintDag" to force printing the dag to /tmp	gareuselesinge	2013-10-07
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Prettyp: avoid useless "let module"	letouzey	2013-09-19