coq - The formal proof system

Age	Commit message (Expand)	Author
2016-07-06	Disallow dependent case on prim records w/o eta	Matthieu Sozeau
2016-07-06	Renaming to more generic has_dependent_elim test	Matthieu Sozeau
2016-07-06	Move is_prim... to Inductiveops and correct Scheme	Matthieu Sozeau
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-12-05	An example in centralizing similar functions to a common place so that	Hugo Herbelin
2015-07-05	Fix handling of primitive projections in VM.	Maxime Dénès
2015-03-25	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin
2015-01-12	Update headers.	Maxime Dénès
2014-08-28	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau
2014-08-14	Fix non-printing of coercions for primitive projections (fixes bug #3433).	Matthieu Sozeau
2014-08-05	A new step in the new "standard" naming policy for propositional hypotheses	Hugo Herbelin
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