coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Potentially unused computation in Goal.	Pierre-Marie Pédrot	2014-03-07
*	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
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Fixing pervasive comparisons	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
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Get rid of the enterl/glist API for Proofview.Goal.	Arnaud Spiwack	2014-02-27
*	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