coq - The formal proof system

Age	Commit message (Expand)	Author
2016-02-09	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-12-15	Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.	Hugo Herbelin
2015-12-05	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin
2015-12-05	Simplifying an instantiation function using subst_of_rel_context_instance.	Hugo Herbelin
2015-12-05	About building of substitutions from instances.	Hugo Herbelin
2015-12-05	An example in centralizing similar functions to a common place so that	Hugo Herbelin
2015-07-07	Univs: bug fix.	Matthieu Sozeau
2015-07-05	Fix handling of primitive projections in VM.	Maxime Dénès
2015-03-25	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin
2015-02-27	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin
2015-02-27	Fixing typo resulting in wrong printing of return clauses for	Hugo Herbelin
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-10-20	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin
2014-10-11	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau
2014-09-13	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin
2014-09-04	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack
2014-08-28	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau
2014-08-14	Fix non-printing of coercions for primitive projections (fixes bug #3433).	Matthieu Sozeau
2014-08-05	A new step in the new "standard" naming policy for propositional hypotheses	Hugo Herbelin
2014-08-03	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau
2014-08-01	Continuing (incomplete) cleaning of Inductiveops.	Hugo Herbelin
2014-08-01	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin
2014-07-03	Cleanup code related to the constraint solving, which sits now outside the	Matthieu Sozeau
2014-06-28	Quick fix of bug #2996 continued (case of inductive types).	Hugo Herbelin
2014-06-26	Deactivate the "Standard Propositions Naming" flag, source of a lot of	Hugo Herbelin
2014-06-25	Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_...	Matthieu Sozeau
2014-06-17	Removing dead code.	Pierre-Marie Pédrot
2014-06-04	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau
2014-06-01	Use of "H"-based names for propositional hypotheses obtained by	Hugo Herbelin
2014-05-09	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau
2014-05-06	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-28	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-20	Check a list length before doing a List.chop (fix #3000)	letouzey
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-11-22	Monomorphization (pretyping)	ppedrot
2012-09-18	Cleaning interface of Util.	ppedrot
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-09-14	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
2012-08-08	Updating headers.	herbelin