coq - The formal proof system

Age	Commit message (Expand)	Author
2011-05-04	First phase removing obsolete support for eta up to conversion in	herbelin
2011-04-29	Fixed a bug causing inconsistent states during proof editting.	aspiwack
2011-04-29	Some comments.	aspiwack
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-08	Applying Tom Prince's patch for build_constant_by_tactic not able to	herbelin
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-18	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
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
2011-02-17	- Use transparency information all the way through unification and	msozeau
2011-02-10	Started to fix the declarative proof mode (C-zar).	aspiwack
2011-02-07	Factorize code of rewrite to make way for a new implementation using the	msozeau
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-12-15	Clenv.connect_clenv without its Evd.fold	letouzey
2010-12-13	Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefined	letouzey
2010-12-10	Attempt to preserve casts during a refine, especially VMcast	letouzey
2010-11-07	Delayed the evar normalization in error messages to the last minute	herbelin
2010-10-25	Fix minor typo in error message (Closes: #2408)	glondu
2010-10-06	Remove open_subgoals field of proof_tree	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
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
2010-07-21	Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proof	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-18	Quick fix for having clenv debug printer working in trunk.	herbelin
2010-06-13	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin
2010-06-09	Fix bug #2317: setoid_rewrite ignored binding lists. Slightly	msozeau
2010-06-09	Automatic introduction of names given before ":" in Lemma's and	herbelin
2010-06-07	Fix comment	glondu
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-05-29	Typo in comment of proof.ml	herbelin
2010-05-19	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey
2010-05-13	Improved the efficiency of evars traverals thanks to a split of	herbelin
2010-05-10	Fix: Pfedit.get_current_goal_context when no goal is focused.	aspiwack
2010-05-10	Removed an evar_merge in clenv_fchain which not only is incorrect but	herbelin
2010-05-05	Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof	pboutill
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack