coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Injection: do not fail when arguments have sort Prop.	Maxime Dénès	2014-04-29
*	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
*	Closing bug #3260	Julien Forest	2014-04-14
*	Cosmetic changes in Equality.	Pierre-Marie Pédrot	2014-03-27
*	Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.	Pierre-Marie Pédrot	2014-03-26
*	Removing Tacmach compatibility layer in Equality.	Pierre-Marie Pédrot	2014-03-26
*	Removing tactic compatibility layer in Equality.	Pierre-Marie Pédrot	2014-03-26
*	Removing Tacmach compatibility layer in Inv.	Pierre-Marie Pédrot	2014-03-26
*	Moving some tactic code to the new engine.	Pierre-Marie Pédrot	2014-03-26
*	Fix test-suite 2255.v	Pierre Boutillier	2014-03-17
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-02
*	Porting Tactics.assumption to the new engine.	ppedrot	2013-11-08
*	Made Proofview.Goal.hyps a named_context.	aspiwack	2013-11-02
*	Less use of the list-based interface for goal-bound tactics.	aspiwack	2013-11-02
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	Clean up a warning.	aspiwack	2013-11-02
*	Cleanup of comments.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Fixing potential evar leak in Equality.	ppedrot	2013-10-05
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Continuing r16621 on injection intro-patterns:	herbelin	2013-07-10
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Making the behavior of "injection ... as ..." more natural:	herbelin	2013-06-02
*	Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an	herbelin	2013-06-02
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Equality: avoid some unprotected List.nth (fix #2837)	letouzey	2013-04-10
*	Restrict (try...with...) to avoid catching critical exn (part 10)	letouzey	2013-03-13
*	Equality: avoid an anomaly about inj_pair2_eq_dec	letouzey	2013-03-12
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of Label	ppedrot	2012-12-18
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18