coq - The formal proof system

Age	Commit message (Expand)	Author
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-04	Fixing previous commit (something strange happened...)	ppedrot
2012-06-04	Replacing some str with strbrk	ppedrot
2012-06-04	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot
2012-06-04	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau
2012-06-01	Cleaning Pp.ppnl use	ppedrot
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
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-04-27	Implicit arguments of Definition are taken from the type when given by the user.	pboutill
2012-04-17	Bug 2733 : { } implicits and Fixpoints	pboutill
2012-03-20	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau
2012-03-20	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin
2012-03-19	Fix bugs related to Program integration.	msozeau
2012-03-14	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau
2012-03-14	Integrated obligations/eterm and program well-founded fixpoint building to to...	msozeau
2012-03-02	Noise for nothing	pboutill
2011-12-17	A pass on warning printings. Made systematic the use of msg_warning so	herbelin
2011-12-12	Proof using ...	gareuselesinge
2011-11-17	Merge subinstances branch by me and Tom Prince.	msozeau
2011-10-11	Various simplifications about constant_of_delta and mind_of_delta	letouzey
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-02-10	Fixpoints are traverse during implicits arguments search to toplevel	pboutill
2011-02-10	Interp a definition with the implicit arguments of its local context	pboutill
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-03	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin
2010-07-27	Fix computation of fix annotation index: only consider assumptions and	msozeau
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-07-16	Amelioration dans Function	jforest
2010-06-29	change the flag "internal" in declare/ind_tables from bool to	vsiles
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin
2010-06-12	Added regression tests for bugs + miscellaneous improvements	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-09	Automatic introduction of names given before ":" in Lemma's and	herbelin
2010-06-08	Fix treatment of {struct x} annotations in presence of generalized	msozeau
2010-05-04	- Fixing bug #2308 about Lemma ... with	vsiles
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2009-12-12	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin