coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-02
*	Fixing abstract tactic by using a dummy name out of a declared proof.	Pierre-Marie Pédrot	2013-11-27
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Remove some occurrences of obsolete operators	Stephane Glondu	2013-11-22
*	Porting Tactics.assumption to the new engine.	ppedrot	2013-11-08
*	Refine now does iota reduction in addition to beta.	aspiwack	2013-11-02
*	Refine: Tactics.New.refine does beta-reduction.	aspiwack	2013-11-02
*	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
*	Fix behaviour of the refine tactic with respect to evars in types.	aspiwack	2013-11-02
*	Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Cleanup of comments.	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	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
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	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
*	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
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	Less "Coq" strings everywhere	letouzey	2013-08-22
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Side effect free implementation of admit (Isabelle's oracle)	gareuselesinge	2013-08-08
*	Fixing #3062. Computation of the value of a fresh identifier was	ppedrot	2013-08-04
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an	herbelin	2013-06-02
*	Fixing buggy backtracking in "intros * pat" with failing "pat".	herbelin	2013-06-02
*	Setting "appcontext" as the default behaviour in Ltac matching.	ppedrot	2013-05-28
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin	2013-03-21
*	Fixing an old pecularity of "red": head betaiota redexes are now	herbelin	2013-03-21
*	Restrict (try...with...) to avoid catching critical exn (part 10)	letouzey	2013-03-13
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22