coq - The formal proof system

Age	Commit message (Expand)	Author
2013-05-06	Small cleaning of Evd interface.	ppedrot
2013-05-03	Removing a redundant function from Evd.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-12	A version of Univ.check_eq with no anomaly for Evd.set_eq_sort	letouzey
2013-03-12	Allowing different types of, not to be mixed, generic Stores through	ppedrot
2013-02-17	Locating errors from consider_remaining_unif_problems if possible	herbelin
2013-01-29	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-11-26	Removed some FIXME related to equality on universes.	ppedrot
2012-11-26	Small cleaning of interface in Univ	ppedrot
2012-11-22	Monomorphization (pretyping)	ppedrot
2012-11-20	Cleaning and small optimization in CList.	ppedrot
2012-11-03	Reversed roles of undefined/defined evars in Evd, thus saving precious	ppedrot
2012-10-29	Removed many calls to OCaml generic equality. This was done by	ppedrot
2012-10-17	univ inconsistency error message gives evidence of a cycle	barras
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-15	Some documentation and cleaning of CList and Util interfaces.	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-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
2012-03-22	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey
2012-03-20	Generalized the use of evar candidates in type inference unification:	herbelin
2012-03-02	Noise for nothing	pboutill
2011-12-17	Added ability to take the type of applied metas into account when	herbelin
2011-12-16	Introducing a notion of evar candidates to be used when an evar is	herbelin
2011-10-26	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey
2011-10-25	Continuing r14585 (ill-typed restriction bug).	herbelin
2011-10-22	Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...	herbelin
2011-10-11	More on r14536 (an unused pattern-matching remained in the commit).	herbelin
2011-10-10	Little code simplification of instantiate_evar in evd.ml	herbelin
2011-10-10	Added information about evar origin in pretty-printing evd for debug	herbelin
2011-10-10	Passed conv_algo to evar_define and move call to solve_refl to	herbelin
2011-08-02	More robust evar_map debugging printer	herbelin
2011-06-21	Cleaning debugging printer relative to new proof engine. In	herbelin
2011-06-12	Added a new flag for freezing evars in tactic unification. Used this	herbelin
2011-05-13	A better procedure for checking presence of undefined evars.	aspiwack
2011-05-04	First phase removing obsolete support for eta up to conversion in	herbelin
2011-03-23	- Remove useless grammar rule	msozeau
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-03-11	- Better error messages taking unif. constraints into account.	msozeau
2011-03-10	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau
2011-03-10	Do not forget conv_pbs when resetting an evm:	msozeau
2011-02-17	- Use transparency information all the way through unification and	msozeau
2010-12-15	Misc improvements about evar_map	letouzey
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey