coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-02	Optimisation of partial applications in the tactic monad.	aspiwack
2013-11-02	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack
2013-11-02	Fix behaviour of the refine tactic with respect to evars in types.	aspiwack
2013-11-02	Small syntax fix to be compatible with Ocaml 3.11.	aspiwack
2013-11-02	Makes the Ltac debugger usable again.	aspiwack
2013-11-02	Document "all:" and "Set Default Goal Selector".	aspiwack
2013-11-02	New option Default Goal Selector.	aspiwack
2013-11-02	Adds a new goal selector "all:".	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	Removes Refine from the dev tools now that the module has been deleted.	aspiwack
2013-11-02	Clean up a warning.	aspiwack
2013-11-02	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-11-02	Cleanup of comments.	aspiwack
2013-11-02	Plug back the declarative mode.	aspiwack
2013-11-02	Small change to the IO monad interface: [val ref : 'a -> 'a ref t]	aspiwack
2013-11-02	A whole new implemenation of the refine tactic.	aspiwack
2013-11-02	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack
2013-11-02	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack
2013-11-02	Bases tactics on an IO monad.	aspiwack
2013-11-02	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack
2013-11-02	Uses Proofview.tclEXTEND more sparingly.	aspiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-11-02	Closure: fix an issue with r16959 spotted by Matthieu	letouzey
2013-10-31	Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)	letouzey
2013-10-31	Fixing Kerpair.hash. Since the beginning, it dit not respect the type	ppedrot
2013-10-31	Future: better doc + restore ~pure optimization	gareuselesinge
2013-10-31	CoqIDE: scroll to the right position if there is an interp error	gareuselesinge
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-31	Efficient filtered functions in Evd. We test that a filter is actually	ppedrot
2013-10-31	Avoiding useless allocations in Closure.	ppedrot
2013-10-30	Various optimizations of Evd.meta_* functions.	ppedrot
2013-10-30	More efficient implementation of [Evd.retract_coercible_metas].	ppedrot
2013-10-29	Optimization in unification: when checking that the head of a term is an	ppedrot
2013-10-29	Useless array-to-list casts in Unification.	ppedrot
2013-10-29	Do not generate useless argument arrays in whd_* functions.	ppedrot
2013-10-29	Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.	ppedrot
2013-10-29	[Reductionops.append_stack_app]: do not allocate a useless array.	ppedrot
2013-10-29	Revert the two last commits. My bad, I messed up git-svn commands...	ppedrot
2013-10-29	Profile only when CAMLRUNPARAM is set.	ppedrot
2013-10-29	Printing heap on every processed sentence.	ppedrot
2013-10-29	Sharing identity evar filters.	ppedrot
2013-10-29	Allocation-friendly version of [Pre_env.push_named].	ppedrot
2013-10-29	Optimizing universes: tail-rec, allocation friendly [compare_leq].	ppedrot
2013-10-29	- install evar printer for debugging	msozeau
2013-10-28	Native compiler: library compilation errors are now non fatal.	mdenes
2013-10-28	Evar leak in "absurd" tactic.	ppedrot
2013-10-28	Removing Evd.undefined_evars.	ppedrot
2013-10-28	Useless array to list conversions in proof/logic.ml.	ppedrot
2013-10-27	Removing useless filter allocation in evar construction.	ppedrot