coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Allowing the "Declare Instance" command anywhere. This was artificially	Pierre-Marie Pédrot	2014-05-01
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25
*	Removing Autoinstance once and for all.	Pierre-Marie Pédrot	2014-04-25
*	Removing useless try-with clauses in Goal.enter variants.	Pierre-Marie Pédrot	2014-04-25
*	Fixing various backtrace recordings.	Pierre-Marie Pédrot	2014-04-25
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Have the feedback bus as a backend for dumping globs.	Carst Tankink	2014-04-10
*	Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...	Pierre Boutillier	2014-04-09
*	Add an option -Q (tentative name).	Guillaume Melquiond	2014-04-08
*	Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...	Guillaume Melquiond	2014-04-07
*	Change handling of loadpath and mlpath.	Guillaume Melquiond	2014-04-06
*	STM: be more resilient to explicit Back + Sideff commands (closes: 3251)	Enrico Tassi	2014-04-02
*	Removing dead code in Tactics.	Pierre-Marie Pédrot	2014-03-31
*	Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.	Pierre-Marie Pédrot	2014-03-26
*	STM: when an error occurs in a worker send back a bunch of states	Enrico Tassi	2014-03-26
*	Adding a Print Strategy vernacular command. It allows to check the	Pierre-Marie Pédrot	2014-03-19
*	STM: make the slave start from the most recent known state	Enrico Tassi	2014-03-18
*	STM: make -async-proofs on work from coqc too	Enrico Tassi	2014-03-18
*	fix compilation with ocaml < 4	Enrico Tassi	2014-03-13
*	STM: perspective (tell the scheduler what the user sees)	Enrico Tassi	2014-03-13
*	STM: move out a couple of submodules	Enrico Tassi	2014-03-13
*	Stm: smarter delegation policy	Enrico Tassi	2014-03-12
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	Using Hashmaps by default in constant and inductive maps. This changes fold and	Pierre-Marie Pédrot	2014-03-07
*	Lets coqtop use a slash	Virgile Prevosto	2014-03-06
*	Using HMaps in Safe_env.environments, hopefully improving performances.	Pierre-Marie Pédrot	2014-03-05
*	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
*	STM: fix Show Script	Enrico Tassi	2014-03-04
*	STM: when finish a task hcons universe constraints	Enrico Tassi	2014-03-04
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Migrate back g_obligations in toplevel	Pierre Letouzey	2014-03-02
*	Useless check when loading notations through import.	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
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	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
*	STM: better messages when checking/finishing tasks	Enrico Tassi	2014-02-26
*	vi2vo: new flag -schedule-vi2vo	Enrico Tassi	2014-02-26
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	STM: backup/restore remote counters	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	Fixing printing of only_parsing notations.	Pierre-Marie Pédrot	2014-02-25
*	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier	2014-02-24
*	Dead Code elimination	Pierre Boutillier	2014-02-24
*	Timeout and Set Default Timeout fixed (closes: #3229)	Enrico Tassi	2014-02-10
*	STM: when a worker is canceled mark the proof as broken	Enrico Tassi	2014-02-10
*	STM: be conservative w.r.t. proofs containing global side effects	Enrico Tassi	2014-02-10