coq - The formal proof system

Age	Commit message (Expand)	Author
2010-12-23	Fix diagram in genarg.mli	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-12-23	Prepare change of nomenclature rawconstr -> glob_constr	glondu
2010-12-23	More precise documentation for instantiate	glondu
2010-12-21	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey
2010-12-19	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin
2010-12-18	Univ: try to avoid a few lookup in the universe graph	letouzey
2010-12-18	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey
2010-12-18	Revert last commit 13723 on Univ : minor gains and more complex code	letouzey
2010-12-17	Univ: an attempt to lazily compact chains of Equiv in a functionnal way	letouzey
2010-12-17	NPeano.modulo : another trick a la "minus" for having a decreasing arg	letouzey
2010-12-17	Cosmetic : let's take advantage of the n-ary exists notation	letouzey
2010-12-17	Nicer log2 function for nat (suggested by Hugo)	letouzey
2010-12-16	Univ: two improvements (speed + space)	letouzey
2010-12-15	Clenv.connect_clenv without its Evd.fold	letouzey
2010-12-15	Evar-related speed-up and clarifications in Class_tactics and Rewrite	letouzey
2010-12-15	Misc improvements about evar_map	letouzey
2010-12-14	Add improved indenters that rely on the current proof state to choose the ind...	gmelquio
2010-12-14	Add navigation items for quickly moving between word occurrences.	gmelquio
2010-12-14	Improved the search/replace dialog box:	gmelquio
2010-12-14	Fix mutex being released from a different thread than it is acquired from.	gmelquio
2010-12-13	Remove an unused function with a Evd.fold in subtac	letouzey
2010-12-13	Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefined	letouzey
2010-12-13	Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometry	letouzey
2010-12-13	Avoid silent loss of data when closing an unsaved buffer.	gmelquio
2010-12-12	Sorry for the mistake in r13702	pboutill
2010-12-10	Attempt to preserve casts during a refine, especially VMcast	letouzey
2010-12-10	First release of Vector library.	pboutill
2010-12-09	Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.	herbelin
2010-12-09	In passing, very quick uniformization of coqdoc headers in a few files.	herbelin
2010-12-09	ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2	letouzey
2010-12-09	Example of a simple ML tactic (Hello world).	fkirchne
2010-12-06	Fixed status of ÷ and × in coqdoc (they were seen as letter instead of symb...	herbelin
2010-12-06	Numbers and bitwise functions.	letouzey
2010-12-06	Use !Pp_control.std_ft for printing grammars	glondu
2010-12-04	Made new comm. model between coq and coqide support '-R foo ""'-style option.	herbelin
2010-12-04	Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).	herbelin
2010-12-04	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin
2010-12-04	Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally,	herbelin
2010-12-04	Better fix to bug #2183 ("moduleid" internal name got exposed to users	herbelin
2010-12-04	Fixing several bugs with links to notation in coqdoc, including bug #2445:	herbelin
2010-12-03	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin
2010-12-03	Redirect stdout to stderr in -ideslave	glondu
2010-12-03	Remove dead code	glondu
2010-12-02	Fixing a bug introduced in r12304 (move of interpretation of	herbelin
2010-12-02	Document new tactics in CHANGES	glondu
2010-12-02	Documentation for tactic constr_eq	glondu
2010-12-02	Add tactic has_evar (#2433)	glondu
2010-12-02	Add tactic is_evar (Closes: #2433)	glondu