coq - The formal proof system

Age	Commit message (Expand)	Author
2014-10-27	Cleaning and documenting Clenv.make_evar_clause	Pierre-Marie Pédrot
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-10-21	Lazily check that an argument is dependent when constructing evar clauses.	Pierre-Marie Pédrot
2014-10-21	Adding an evar version of the make_clenv function.	Pierre-Marie Pédrot
2014-09-17	Be more conservative and keep the use of eq_constr in pretyping/ functions.	Matthieu Sozeau
2014-09-17	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-10	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin
2014-05-06	Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-03-26	Moving some tactic code to the new engine.	Pierre-Marie Pédrot
2014-03-01	Fixing pervasive comparisons	Pierre-Marie Pédrot
2013-10-29	Do not generate useless argument arrays in whd_* functions.	ppedrot
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-09-25	Removing useless evar-related stuff.	ppedrot
2013-06-04	Backtrack on unneeded change of interface for pose_metas_as_evars.	msozeau
2013-06-04	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau
2013-05-03	Removing a redundant function from Evd.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-02-17	Added propagation of evars unification failure reasons for better	herbelin
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-11-25	Monomorphization (proof)	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-07-20	Reductionops refactoring	pboutill
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2012-03-14	Second step of integration of Program:	msozeau
2012-03-02	Noise for nothing	pboutill
2011-10-11	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin
2011-06-21	Cleaning debugging printer relative to new proof engine. In	herbelin
2011-06-13	Added a flag to restrict conversion in tactic unification on the	herbelin
2011-06-10	Moved allow_K to a unification flag	herbelin
2011-05-04	First phase removing obsolete support for eta up to conversion in	herbelin
2011-03-10	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau
2011-03-07	Reverted commit r13893 about propagation of more informative	herbelin
2011-03-07	Added propagation of evars unification failure reasons for better	herbelin
2011-02-22	Try to fix the behavior of clenv_missing used when declaring hints	letouzey
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-15	Clenv.connect_clenv without its Evd.fold	letouzey
2010-11-07	Delayed the evar normalization in error messages to the last minute	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-17	In the computation of missing arguments for apply, accept that the	herbelin
2010-08-02	Fix [clenv_missing] to compute a better approximation of missing	msozeau
2010-07-24	Updated all headers for 8.3 and trunk	herbelin