coq - The formal proof system

Age	Commit message (Expand)	Author
2013-10-23	Small optimizations in unification.	ppedrot
2013-10-23	Removing List.mem in Namegen. We may choose a better fitted datastructure tha...	ppedrot
2013-10-22	Removing some generic equalities.	ppedrot
2013-10-22	Moving potentially costly computation from exception raising to message	ppedrot
2013-10-22	Removing useless array-to-list and converse casts used in	ppedrot
2013-10-22	Optimizing evar filters. It seems to cost quite a lot in unification,	ppedrot
2013-10-22	Various optimizations in Constr, such as term sharing and allocation	ppedrot
2013-10-08	Small code cleaning in Evarutil.	ppedrot
2013-10-06	Removing useless evar code.	ppedrot
2013-10-06	Removing uses of Evar.add in class-related functions.	ppedrot
2013-10-05	Removing dubious use of evarmap manipulating functions in printing	ppedrot
2013-10-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-25	Removing useless evar-related stuff.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-18	Removing the last global evar generation in Term_dnet. The very	ppedrot
2013-09-18	Removing unused code from Term_dnet.	ppedrot
2013-09-18	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot
2013-09-18	Taming the simpl evar hack that used to use negative evars.	ppedrot
2013-09-12	Unplugging Autoinstance. The code is still here if someone wishes	ppedrot
2013-09-05	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot
2013-09-05	Documentation of Evd.	ppedrot
2013-09-05	Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.	ppedrot
2013-09-03	Partly replacing list-based access functions in Evd. This is still	ppedrot
2013-08-25	Removing association lists in Reductionops. Btw, defining the dual of the	ppedrot
2013-08-25	Actually using the domain function for maps.	ppedrot
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-08-25	Replacing lists by sets in clear tactic.	ppedrot
2013-08-22	Nicer code concerning dirpaths and modpath around Lib	letouzey
2013-08-22	Misc changes around coqtop.ml :	letouzey
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