coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Noise for nothing	pboutill	2012-03-02
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10
*	Extraction: avoid internal eta-reduction (fix #2570)	letouzey	2011-12-08
*	Extraction: try to avoid issues with an Include directly inside a .v	letouzey	2011-11-30
*	Extraction: typo in last commit	letouzey	2011-11-29
*	Extraction: Richer patterns in matchs as proposed by P.N. Tollitte	letouzey	2011-11-28
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Extraction Implicit: fix the numbering of constructor arguments	letouzey	2011-09-05
*	Extraction: allow extraction of records with anonymous fields (fix #2555)	letouzey	2011-08-25
*	Extract_env: generic = on prec_declaration replaced by prec_declaration_equal	puech	2011-07-29
*	Extraction: replace generic = on mutual_inductive_body by mib_equal	puech	2011-07-29
*	Set Extraction KeepSingleton: an option for not decapsulating singleton types	letouzey	2011-07-04
*	Extraction: in haskell, __ may have any type, no need to unsafeCoerce it	letouzey	2011-07-04
*	Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)	letouzey	2011-07-04
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Extraction: avoid lots of late mind_of_kn	letouzey	2011-05-19
*	Extraction: global reference should be indexed on their user part (fix #2540)	letouzey	2011-05-19
*	Extraction: avoid printing of Recursive Extraction in coqide's console	letouzey	2011-05-18
*	Fixed my last patch: these files no longer use nat_beq (automatically	vsiles	2011-05-16
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	Modularization of BinNat + fixes of stdlib	letouzey	2011-05-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	Extraction: allow extraction foo when foo is an alias notation	letouzey	2011-05-05
*	Extraction: nicer error when a toplevel module has no body (#2525)	letouzey	2011-04-15
*	Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)	letouzey	2011-04-15
*	Extraction: opaque terms are not traversed anymore by default	letouzey	2011-04-13
*	Extraction: unfolds the let-in created by Program when handling "match"	letouzey	2011-04-07
*	Extraction: avoid some useless Obj.magic by fixing my ML type unifier	letouzey	2011-04-07
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Extraction: customized inductives are always standard	glondu	2011-03-31
*	Extraction: a warning when an opaque constant is enterred	letouzey	2011-03-07
*	Extraction: fix printing of haskell modular names	letouzey	2011-03-07
*	Extraction: avoid printing unused mutual fix components (fix #2477)	letouzey	2011-03-07
*	A new command "Separate Extraction"	letouzey	2011-03-07
*	Extraction: improved indentation of extracted code (fix #2497)	letouzey	2011-03-04
*	Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)	letouzey	2011-02-25
*	Fix indentation of default pattern in haskell case (bug #2476)	letouzey	2011-02-25
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)	letouzey	2011-01-07
*	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey	2010-12-21
*	Extraction: allow to use Extraction Inline / NoInline even from under a section.	letouzey	2010-10-06
*	Dead code in extraction	letouzey	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20