coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-03	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau
2014-08-01	Continuing (incomplete) cleaning of Inductiveops.	Hugo Herbelin
2014-08-01	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin
2014-06-01	Use of "H"-based names for propositional hypotheses obtained by	Hugo Herbelin
2014-05-31	Dead code + typo.	Hugo Herbelin
2014-05-06	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2012-08-08	Updating headers.	herbelin
2012-03-02	"Let in" in pattern hell, one more iteration	pboutill
2012-01-16	Inductiveops.nb_*{,_env} cleaning	pboutill
2011-12-18	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin
2011-04-06	A few extra combinators about rel_declaration/named_declaration + a bit of doc	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-07-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-10-07	fixing r11433 again:	barras
2008-07-25	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin
2007-03-15	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin
2006-10-01	Ajout allowed_sorts	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-04-27	- Distinction explicite des parties paramètres et arguments dans le type	herbelin
2006-01-30	Fonctions retournant les arits des constructeurs et inductifs	herbelin
2005-02-18	Moving subst_inductive from tacinterp to inductiveops for better for reuse in...	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-14	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot
2004-08-24	Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-11-18	Ajout mis_constructor_nargs_env	herbelin
2002-12-13	correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...	letouzey
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-06-13	Ajout map_inductive_type et map_ind_family	herbelin
2002-02-14	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras
2002-02-07	petit nettoyage de kernel/inductive	barras
2001-11-20	Ajout make_arity_signature	herbelin
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras