coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	still some more dead code removal	letouzey	2012-10-06
*	remove Refiner.abstract_tactic and similar	letouzey	2012-10-06
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06
*	Proof_type: rule now degenerates to prim_rule	letouzey	2012-10-06
*	Clean-up : no more Proof_type.proof_tree	letouzey	2012-10-06
*	Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box	letouzey	2012-10-06
*	Remove the unused "intel" field in Proof.proof_state	letouzey	2012-10-02
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Use the library function List.substract in prev commit	letouzey	2012-10-02
*	Added a new tactical infoH tac, that displays the names of hypothesis created...	courtieu	2012-10-01
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14