coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	stm: (initial) support for -coq-slaves	gareuselesinge	2013-08-08
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Fixing bug #3030.	ppedrot	2013-06-06
*	Backtrack on unneeded change of interface for pose_metas_as_evars.	msozeau	2013-06-04
*	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau	2013-06-04
*	Removing a useless location in ltac trace mechanism.	ppedrot	2013-05-30
*	Getting rid of LtacLocated exception transformer.	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
*	Fixing ocamldoc compilation.	ppedrot	2013-05-06
*	Removing a redundant function from Evd.	ppedrot	2013-05-03
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Fixing #2968. This is quite brittle though, because we are messing	ppedrot	2013-04-16
*	Allow catching of WrongAbstractionType, fixing a regression from 8.4	msozeau	2013-04-05
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	another Errors.push in a exception reraise	letouzey	2013-03-16
*	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey	2013-03-14
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey	2013-03-13
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	No reason a priori for using unfiltered env for printing	herbelin	2013-01-29
*	Fixing bug #2969 (admit failing after Grab Existential Variables due	herbelin	2013-01-29
*	Fixed synchronicity of filter with evar context in new_goal_with.	herbelin	2013-01-29
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Added backtrace information to anomalies	ppedrot	2013-01-28
*	Reductionops: whd_state_gen can take and answers a cst_stack too	pboutill	2013-01-24
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Yet a new reduction tactic in Coq : cbn	pboutill	2012-12-21
*	Modulification of name	ppedrot	2012-12-18
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Stringset and Stringmap to String namespace.	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Monomorphization (proof)	ppedrot	2012-11-25
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Fix bug #2892	letouzey	2012-10-22