coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Removing now useless merging primitives from Evd.	ppedrot	2013-08-04
*	Small fixes due to the arrival of OCaml 3.12.	ppedrot	2013-08-03
*	Fixing #3088. Translation from globconstrs to patterns was forgetting	ppedrot	2013-08-01
*	Added printing of instance priority to the Print Instances command.	ppedrot	2013-08-01
*	- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...	msozeau	2013-07-19
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Using the whole tactic environment while Pretyping.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	- Keep the refinement of existing evars comming from unification with a rewri...	msozeau	2013-06-19
*	One more fix for rewrite: disallow resolving of the (partial) constraints	msozeau	2013-06-12
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	Do not compute fallback eagerly in Evarconv	pboutill	2013-05-30
*	export Unification.abstract_list_all_with_dependencies	pboutill	2013-05-30
*	Why not going inside fixpoint definition with appcontext ?	pboutill	2013-05-30
*	comments in mli	pboutill	2013-05-30
*	Pushing lazy lists into Ltac. Now, the control flow is explicit	ppedrot	2013-05-28
*	Code cleaning in Matching.	ppedrot	2013-05-24
*	Mini documentation (evar_absorb_arguments).	herbelin	2013-05-14
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	"change ... in ..." and "simpl ... in ..." now consider nested	herbelin	2013-05-14
*	Fixing a regression in unification introduced in r16205 (error raised	herbelin	2013-05-14
*	Removing Gmap from Classops. Fold order only mattered for printing.	ppedrot	2013-05-14
*	Removing useless uses of Gmap.	ppedrot	2013-05-14
*	Replacing compatibility layer for Fmap in Typeclasses. Code was	ppedrot	2013-05-14
*	More semantical-friendly function.	ppedrot	2013-05-14
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Fixing a source of evars leak, revealed by contrib QuicksortComplexity	herbelin	2013-05-11
*	Little oversight in commit r16489 (fix for bug #3036).	herbelin	2013-05-10
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	A few comments in evarconv.mli.	herbelin	2013-05-09
*	Uniformization: isevars -> evdref/sigma/evd	herbelin	2013-05-09
*	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot	2013-05-08
*	Protection against "Bad recursive type" in w_unify0 (bug #3036).	herbelin	2013-05-08
*	Fixing ocamldoc compilation.	ppedrot	2013-05-06
*	Small cleaning of Evd interface.	ppedrot	2013-05-06
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Hack to solve a "Bad recursive type" anomaly.	herbelin	2013-05-05
*	Removing a redundant function from Evd.	ppedrot	2013-05-03
*	Fix wrong computation of dependency signature in cases raising an uncaught ex...	msozeau	2013-04-30
*	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
*	Fix #3001 (rename arg of global cst inside section)	gareuselesinge	2013-04-18
*	Matching patterns: fixed allow_partial_app which was not working on	herbelin	2013-04-17
*	Fix of r16257 in r16205 for "errors raised by check_evar_instance were	herbelin	2013-04-17
*	Like in r16346, do not filter local definitions (here in the	herbelin	2013-04-17
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03