coq - The formal proof system

Age	Commit message (Expand)	Author
2020-09-07	Remove dead code in clenv-generating functions.	Pierre-Marie Pédrot
2020-09-06	Merge PR #12976: Remove clenv chaining in Equality	Hugo Herbelin
2020-09-06	Merge PR #12980: Simplify the implementation of Elim	Hugo Herbelin
2020-09-04	Remove a unused function from the Clenv API.	Pierre-Marie Pédrot
2020-09-04	Remove the last use of clenv_fchain in Equality.	Pierre-Marie Pédrot
2020-09-04	Inline the last use of apply_on_clause in Equality.	Pierre-Marie Pédrot
2020-09-04	Remove a useless use of clenv_fchain in Equality.	Pierre-Marie Pédrot
2020-09-04	Merge PR #12969: CI: build Iris examples instead of lambda-Rust	coqbot-app[bot]
2020-09-04	Statically enforce that elim is passed a fully applied inductive type.	Pierre-Marie Pédrot
2020-09-04	Restrict a spurious call to a reduction to a quantified inductive type.	Pierre-Marie Pédrot
2020-09-04	Defunctionalize the mk_elim creation in Elim.	Pierre-Marie Pédrot
2020-09-04	Enforce the argument of elim functions to be a variable.	Pierre-Marie Pédrot
2020-09-04	Merge PR #12893: Fix incorrect debruijn handling when Record calls maybe_unif...	coqbot-app[bot]
2020-09-04	Merge PR #12900: [bench] Also upload the raw timing files, etc	Pierre-Marie Pédrot
2020-09-04	Merge PR #12912: Fix algebraic comparison with sprop on one side	Pierre-Marie Pédrot
2020-09-03	Merge PR #12953: Add :math: around math	coqbot-app[bot]
2020-09-03	[bench] Only upload some files	Jason Gross
2020-09-03	[bench] Also upload the raw timing files, etc	Jason Gross
2020-09-03	Fix incorrect debruijn handling when Record calls maybe_unify_params_in	Gaëtan Gilbert
2020-09-03	Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay them	Pierre-Marie Pédrot
2020-09-03	Merge PR #12956: Perform an inversion of control in hint validation for eapply.	coqbot-app[bot]
2020-09-03	Merge PR #12876: Namegen.visible_ids: fixing what seems to be typos	Pierre-Marie Pédrot
2020-09-03	Merge PR #12973: Random cleanup around the data structures used in Equality	Hugo Herbelin
2020-09-03	Merge PR #12899: [bench] Update bench script with better urls and more info	Pierre-Marie Pédrot
2020-09-03	Add Equations overlay	Maxime Dénès
2020-09-03	Comment AllowedEvars API	Maxime Dénès
2020-09-02	More efficient data structure for allowed evars	Maxime Dénès
2020-09-02	Abstract type for allowed evars	Maxime Dénès
2020-09-02	Replace `frozen` by `allowed` evars in evarconv, and delay them	Maxime Dénès
2020-09-02	Merge PR #12943: Move Elim-specific code	Hugo Herbelin
2020-09-02	Remove the opening of CErrors in Elim.	Pierre-Marie Pédrot
2020-09-02	Code deduplication in Elim.	Pierre-Marie Pédrot
2020-09-02	Factorize the only uses of internal API in Elim for Inv.	Pierre-Marie Pédrot
2020-09-02	Make the Elim.branch_args type opaque.	Pierre-Marie Pédrot
2020-09-02	Further remove the type Elim.branch_assumptions.	Pierre-Marie Pédrot
2020-09-02	Remove unused API from Elim.	Pierre-Marie Pédrot
2020-09-02	Document the Equality.equality type in the ML file.	Pierre-Marie Pédrot
2020-09-02	Remove redundant data from the equality eliminator datatype.	Pierre-Marie Pédrot
2020-09-02	Do not look for a quantified inductive type in intropattern injection.	Pierre-Marie Pédrot
2020-09-02	Use a dedicated type for equality elimination.	Pierre-Marie Pédrot
2020-09-02	fix grepping for the Iris commit	Ralf Jung
2020-09-02	CI: build Iris examples instead of lambda-Rust	Ralf Jung
2020-09-02	Merge PR #12883: Use a faster algorithm to check for class existence.	coqbot-app[bot]
2020-09-01	Merge PR #12872: Unify the shelves	Pierre-Marie Pédrot
2020-09-01	Unify the shelves	Maxime Dénès
2020-09-01	Merge PR #12892: Update update_global_env usage	Pierre-Marie Pédrot
2020-09-01	Merge PR #12961: [declare] Return both declared constants in Derive path.	coqbot-app[bot]
2020-09-01	Merge PR #12962: Add zarith to the include path for ocamldebug-coq	coqbot-app[bot]
2020-08-31	Add zarith to the include path for ocamldebug-coq	Jasper Hugunin
2020-08-31	[declare] Return both declared constants in Derive path.	Emilio Jesus Gallego Arias