coq - The formal proof system

Age	Commit message (Expand)	Author
2011-08-01	Term: simplify compare_constr by removing calls to decompose_app	puech
2011-08-01	fixed bug 2580. Quick fix: copy emitcodes before patching it	barras
2011-07-29	Extraction: replace generic = on mutual_inductive_body by mib_equal	puech
2011-07-29	Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Term	puech
2011-07-29	Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...	puech
2011-07-29	Hahtbl_alt: separate generic combine functions	puech
2011-07-29	Environ: generic equality on named_context replaced by named_context_equal	puech
2011-07-29	Term: added function eq_named_declaration	puech
2011-07-29	Indtypes: remove useless and wrong generic equality test on constr array	puech
2011-07-29	Term: slight reorganization of the file	puech
2011-07-29	Term_typing, Typeops: replace some generic '=' on constr by eq_constr	puech
2011-07-29	Term: Refactoring of hashconsing	puech
2011-07-29	argument renaming in liftn (match with usual terminology)	puech
2011-07-04	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey
2011-05-17	Modops: the strengthening functions can work without any env argument	letouzey
2011-05-11	Print Module (Type) M now tries to print more details	letouzey
2011-04-19	Fix thumb2-related build error	glondu
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	- Remove create_evar_defs	msozeau
2011-04-13	Fix merge.	msozeau
2011-04-13	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-12	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey
2011-04-08	Replaced printing number of ill-typed branch by printing name of constructor	herbelin
2011-04-06	A few extra combinators about rel_declaration/named_declaration + a bit of doc	herbelin
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-04-01	CHANGES: a word about recent changes in coqide, about Ctrl-C in vm	letouzey
2011-04-01	Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)	letouzey
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-03-08	adding eta in the vm	bgregoir
2011-03-05	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin
2011-03-05	Starting being more explicit on the reasons why module subtyping fails.	herbelin
2011-03-05	Fixed a "feature" about subtyping records: one was expected not only	herbelin
2011-02-24	Mod_subst: improving sharing of subst_mps	letouzey
2011-02-23	Some more simplification in Mod_subst	letouzey
2011-02-17	- Use transparency information all the way through unification and	msozeau
2011-02-11	Mod_typing: some refactoring (common parts about MSEapply and co)	letouzey
2011-02-11	Safe_typing: some refactoring (avoiding copy-paste of record definitions)	letouzey
2011-02-11	Mod_subt: some more refactoring, substitution is also separated in two tables	letouzey
2011-02-11	Mod_subst: split delta_resolver in two tables (mp / kn)	letouzey
2011-02-11	compatibility <3.12 (Map.exists Map.singleton)	pboutill
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2011-01-27	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey
2011-01-25	Rewrite sort_universes to minimize the number of universes	glondu
2011-01-11	In univ.ml, put universe_level primitives in its their own sub-module	glondu
2011-01-11	Add "Print Sorted Universes"	glondu
2011-01-11	More coherent comment ordering	glondu
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