coq - The formal proof system

Age	Commit message (Expand)	Author
2016-04-27	Reformatting + removal of some useless data + some cut-elimination	Hugo Herbelin
2016-03-12	A more explicit name to the asymmetric boolean flag.	Hugo Herbelin
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-09-02	Removing more association lists in Constrintern.	ppedrot
2013-03-13	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey
2012-12-14	Modulification of identifier	ppedrot
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	remove many excessive open Util & Errors in mli's	letouzey
2012-05-29	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey
2012-05-29	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	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-05-15	Notations are back in the "in" clause of pattern matching.	pboutill
2012-04-12	"A -> B" is a notation for "forall _ : A, B".	pboutill
2012-03-20	Fixing bug #2724 (using notations with binders in cases patterns	herbelin
2012-03-02	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill
2012-03-02	Noise for nothing	pboutill
2012-02-29	In the syntax of pattern matching, "in" clauses are patterns.	pboutill
2012-01-19	Boolean Option Patterns Compatibility	pboutill
2012-01-16	Parameters in pattern first step.	pboutill
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
2011-08-30	Quick improvement of some error messages related to module application	herbelin
2011-07-22	Add a syntax entry for fully applied constructor pattern	pboutill
2011-06-12	Rather quick hack to avoid using notations involving "Type" when	herbelin
2011-02-11	Annotations at functor applications:	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	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-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-14	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin
2010-06-08	Fix treatment of {struct x} annotations in presence of generalized	msozeau
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-03-29	Several bug-fixes and improvements of coqdoc	herbelin
2010-01-17	Variant !F M for functor application that does not honor the Inline declarations	letouzey
2010-01-07	Include can accept both Module and Module Type	letouzey
2009-12-12	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin
2009-12-07	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-18	Module subtyping : allow many <: and module type declaration with <:	letouzey
2009-11-16	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey