coq - The formal proof system

Age	Commit message (Expand)	Author
2013-08-20	Universe counters on slaves are in sync with master	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge
2013-08-04	Removing useless casts between arrays and lists.	ppedrot
2013-08-04	Removing now useless merging primitives from Evd.	ppedrot
2013-08-03	Small fixes due to the arrival of OCaml 3.12.	ppedrot
2013-08-01	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-07-19	- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...	msozeau
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-06-24	Using the whole tactic environment while Pretyping.	ppedrot
2013-06-22	Generalizing the use of maps instead of lists in the interpretation	ppedrot
2013-06-19	- Keep the refinement of existing evars comming from unification with a rewri...	msozeau
2013-06-12	One more fix for rewrite: disallow resolving of the (partial) constraints	msozeau
2013-06-05	Replacing lists by maps in matching interpretation.	ppedrot
2013-05-30	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-28	Pushing lazy lists into Ltac. Now, the control flow is explicit	ppedrot
2013-05-24	Code cleaning in Matching.	ppedrot
2013-05-14	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-12	Use the Hook module here and there.	ppedrot
2013-05-11	Fixing a source of evars leak, revealed by contrib QuicksortComplexity	herbelin
2013-05-10	Little oversight in commit r16489 (fix for bug #3036).	herbelin
2013-05-09	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-08	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-06	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-05	Hack to solve a "Bad recursive type" anomaly.	herbelin
2013-05-03	Removing a redundant function from Evd.	ppedrot
2013-04-30	Fix wrong computation of dependency signature in cases raising an uncaught ex...	msozeau
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-22	code simplifications concerning Summary	letouzey
2013-04-18	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-17	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