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-14	Internalization of pattern is done in two phases.	pboutill
2012-06-04	Replacing some str with strbrk	ppedrot
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
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	Glob_term now mli-only, operations now in Glob_ops	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-04-06	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin
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-20	Notations with binders: Accepting using notations for functional terms	herbelin
2012-01-19	Boolean Option Patterns Compatibility	pboutill
2012-01-16	Parameters in pattern first step.	pboutill
2011-12-16	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin
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-06-08	Make Notation works with anonymous-level "Type".	herbelin
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	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-12-04	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-29	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin
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-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	Remove the svn-specific $Id$ annotations	letouzey
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-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
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