coq - The formal proof system

Age	Commit message (Expand)	Author
2013-06-21	Splitted up Genarg in four different levels:	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-18	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot
2013-06-18	Removing the various glob/subst/interp registering functions for	ppedrot
2013-06-18	Implementing a new interface for Genarg, with centralized data	ppedrot
2013-06-18	Now glob_sign and interp_sign only depend on structures defined	ppedrot
2013-06-12	Added Genarg as generic argument type.	ppedrot
2013-06-12	Changing the type of Ltac values. Now they are toplevel generic	ppedrot
2013-06-06	More comments in Genarg.	ppedrot
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-11-25	Monomorphization (interp)	ppedrot
2012-11-25	More equality functions	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2012-05-29	slim down a bit genarg.ml (pr_intro_pattern forgotten there)	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-03-18	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin
2012-03-02	Noise for nothing	pboutill
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-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-19	Made the interpretation levels rlevel/glevel/tlevel truly phantom	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-06-07	- Added two new introduction patterns with the following temptative syntaxes:	herbelin
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-18	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin
2008-04-04	Quelques améliorations des intro patterns:	herbelin
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-07-09	More natural notation for intro pattern: @a -> ?a	glondu
2007-07-06	New intro pattern "@A", which generates a fresh name based on A.	glondu
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2006-11-20	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin
2006-06-08	Changement du type d'argument 'TacticArgType X' en un type	herbelin
2006-06-07	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-01-16	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom	herbelin
2005-12-26	Petite correction nom QuantHypArgType suite suppression traducteur	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin