coq - The formal proof system

Age	Commit message (Expand)	Author
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2010-01-04	Few misc. updates.	herbelin
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-18	Const_omega: look for S in Init only (avoid future clash with S of Numbers)	letouzey
2009-12-16	correction de la nouvelle option pour functional induction	jforest
2009-12-16	adding an option functional_induction_rewrite_dependent to make functional in...	jforest
2009-12-12	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-12-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
2009-12-08	Fix the build of coq via ocamlbuild	letouzey
2009-12-08	Sos.ml: no more warnings	letouzey
2009-12-02	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin
2009-12-02	Remove interface plugin	glondu
2009-12-01	Continuing r12485-12486 (cleaning around name generation)	herbelin
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-26	Fixing xml theory file export (was not consistent with coqdoc file	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
2009-11-12	Oops, nf_evar_defs just changed to nf_evar_map.	msozeau
2009-11-12	Don't forget to normalize everything w.r.t. evars (fixes bug #2103).	msozeau
2009-11-12	Repair interpretation of numeral for BigQ, add a printer (close #2160)	letouzey
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-10	use only why-dp, support for z3	marche
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-11-03	OrderedType implementation for various numerical datatypes + min/max structures	letouzey
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Make usage of Dyn explicit	glondu
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-09	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-10-07	Fix for missing hypotesae in XML proof tree export.	cek
2009-10-04	Removal of trailing spaces.	serpyc
2009-10-03	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-18	micromega: better handling of exponentiation + correction of test-suite termi...	fbesson
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-15	Dont't forget to update the state or an obligation tactic assignment may	msozeau
2009-09-15	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau
2009-09-14	Backtrack on the forced discharge of type class variables introduced	msozeau
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin