coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Was missing a potential application of subtyping	msozeau	2011-11-17
*	Adding postprocessing to remove "commutative cuts" expansions in	herbelin	2011-11-16
*	Changed the way find_dependencies_signature is working so that it	herbelin	2011-11-16
*	De Bruijn indices bug in pattern matching compilation in the presence	herbelin	2011-11-16
*	Old generalization bug in pattern-matching: names were considered the	herbelin	2011-11-16
*	Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).	herbelin	2011-11-16
*	Old typing bug in pattern-matching compilation (apparently w/o	herbelin	2011-11-16
*	Specialization of tomatch in pattern-matching compilation was done too	herbelin	2011-11-16
*	A bit of documentation around cases.ml + ML modules uselessly open	herbelin	2011-11-16
*	Completed list of theories targets	herbelin	2011-11-16
*	Suppression fichier Case8.v redondant	herbelin	2011-11-16
*	Fixing beautification of "thm_token" (missing space) + improvements.	herbelin	2011-11-16
*	Fixing association of wrong "as"-pattern name when expanding	herbelin	2011-11-16
*	Fixing dependencies lifting bug in pattern-matching compilation	herbelin	2011-11-16
*	Bug 2637: patches to make slightly easier to write programs that use coq code...	pboutill	2011-11-14
*	Bug 2636 - Move string_of_ppcmds to Pp	pboutill	2011-11-14
*	Fixed ocamlbuild compilation (Tom Prince)	ppedrot	2011-11-09
*	Refined second_order_matching so that a constraint on which	herbelin	2011-11-08
*	optimization: memoization for is_open_canonical_projection	gareuselesinge	2011-11-08
*	Improved check is_open_canonical_projection	gareuselesinge	2011-11-08
*	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey	2011-11-07
*	Fixed xml-light handling of whitespace not compliant with XML standard: it st...	ppedrot	2011-11-07
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Fixing tactic remember not correctly checking preservation of typing	herbelin	2011-11-06
*	Also sprach CoqIDE (in XML)	ppedrot	2011-11-06
*	Fixed nasty bug when empty PCData, confusion no string vs. empty string	ppedrot	2011-11-06
*	More XML marshalling functions	ppedrot	2011-11-06
*	Added XML dependencies into Makefile	ppedrot	2011-11-06
*	Partialliy added XML marshalling to ide_intf	ppedrot	2011-11-06
*	Added XML manipulation tools to compilation chain	ppedrot	2011-11-06
*	Added XML manipulation basics (modified from xml-light)	ppedrot	2011-11-06
*	Added missing printing debug functions in IDE interface	ppedrot	2011-11-05
*	Auto: removal of ?use_core_db obsolete now that we have nocore	letouzey	2011-11-04
*	Cleaning a little bit the files talking about descriptions: avoiding	herbelin	2011-11-03
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Added Add LoadPath in coqdep lexer (but not in coqdep itself by lack of time).	herbelin	2011-10-29
*	Fixed broken globalization of identifiers containing utf8 letters	herbelin	2011-10-29
*	Added checksums to glob files and warned about possibly missing	herbelin	2011-10-29
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Remove avoidable use of GDynamic	glondu	2011-10-27
*	Deactivating second-order pattern-matching in evarconv for 8.4.	herbelin	2011-10-26
*	Fix configuration box bug in recursive call	pboutill	2011-10-26
*	Coq_makefile handles .mlpack files	pboutill	2011-10-26
*	Coqdep handles .mlpack	pboutill	2011-10-26
*	Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)	letouzey	2011-10-26
*	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey	2011-10-26
*	Environ.set_universes is dead code	letouzey	2011-10-26
*	Mod_subst: some simplifications, some more significant names to functions, etc	letouzey	2011-10-26
*	Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo	letouzey	2011-10-26
*	Makefile install rule fix	pboutill	2011-10-26