coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	Tacinterp: fewer Proofview.Goal.enterl.	Arnaud Spiwack	2014-02-25
*	cbn understands Arguments	Pierre Boutillier	2014-02-24
*	Stack operations of Reductionops in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	More sharing in Logic, together with some code cleaning.	Pierre-Marie Pédrot	2014-02-21
*	TC: honor the use_typeclasses flag in pretyping	Enrico Tassi	2014-02-12
*	STM: fix valid_id coming from Qed errors	Enrico Tassi	2014-02-10
*	Tracking memory misallocation by trying to improve sharing.	Pierre-Marie Pédrot	2014-02-03
*	Fixing backtrace reporting.	Pierre-Marie Pédrot	2014-02-02
*	Typos in comment.	Arnaud Spiwack	2014-01-31
*	Fixing backtrace handling here and there.	Pierre-Marie Pédrot	2014-01-30
*	Useless Array.of_list	Pierre-Marie Pédrot	2014-01-10
*	Exporting the full pretyper options in Goal.constr_of_raw.	Pierre-Marie Pédrot	2014-01-10
*	Algebraized "No such hypothesis" errors	Pierre-Marie Pédrot	2014-01-06
*	Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...	Arnaud Spiwack	2014-01-06
*	Proof_using: new syntax + suggestion	Enrico Tassi	2014-01-05
*	Proof_global: Simpler API for proof_terminator	Enrico Tassi	2014-01-04
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Fixing backtrace registering of various tactic-related try-with blocks.	Pierre-Marie Pédrot	2013-12-11
*	Fix Admitted.	Arnaud Spiwack	2013-12-04
*	Proof_global: fix start_proof comment after the preceding commits.	Arnaud Spiwack	2013-12-04
*	Factoring(continued).	Arnaud Spiwack	2013-12-04
*	Refactoring: storing more information in the terminator closure.	Arnaud Spiwack	2013-12-04
*	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack	2013-12-04
*	Allow proofs to start with dependent goals.	Arnaud Spiwack	2013-12-04
*	Fixing ltac constr variable handling in refine.	Pierre-Marie Pédrot	2013-11-30
*	Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not	Hugo Herbelin	2013-11-29
*	Useless computation in Goal handle augmentation.	ppedrot	2013-11-12
*	Do not print tactic notation names at each interpretation step.	ppedrot	2013-11-12
*	Partial applications in Goal.	ppedrot	2013-11-09
*	Rewriting the proof monad mechanism. Now it uses pure OCaml code, without	ppedrot	2013-11-07
*	Less partial applications in Vars, as well as better memory allocation.	ppedrot	2013-11-06
*	Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same time	ppedrot	2013-11-05
*	Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...	aspiwack	2013-11-04
*	Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...	aspiwack	2013-11-04
*	Allowing proofs starting with a non-empty evarmap.	ppedrot	2013-11-04
*	A try/with was catching every exception.	aspiwack	2013-11-02
*	Update comments.	aspiwack	2013-11-02
*	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	aspiwack	2013-11-02
*	Fix destruct: nf_evar prior to tactic interpretation.	aspiwack	2013-11-02
*	Add primitives in Goal.V82 to access the goal in nf_evar'd form.	aspiwack	2013-11-02
*	Adds a tactic give_up.	aspiwack	2013-11-02
*	A tactic shelve_unifiable.	aspiwack	2013-11-02
*	Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ...	aspiwack	2013-11-02
*	Adds a shelve tactic.	aspiwack	2013-11-02
*	bootstrap/Monad.v: implements the writer monad in continuation passing style.	aspiwack	2013-11-02
*	bootstrap/Monad.v: implements the environment monad in continuation passing s...	aspiwack	2013-11-02