coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-08	Dropping the misleading int argument of Pp.h.	Hugo Herbelin
2020-10-02	Merge PR #13106: Remove the forward class hint feature.	coqbot-app[bot]
2020-09-30	Remove the forward class hint feature.	Pierre-Marie Pédrot
2020-09-29	Adding a few tacticals for the purpose of porting funind to new proof engine.	Hugo Herbelin
2020-09-23	Merge PR #12977: Statically ensure that only polymophic hint terms come with ...	coqbot-app[bot]
2020-09-23	Merge PR #12847: Tactics inversion and replace work with eq in type	Pierre-Marie Pédrot
2020-09-18	Remove unused API from Dn.	Pierre-Marie Pédrot
2020-09-18	Clean up a bit the implemenation of dnets.	Pierre-Marie Pédrot
2020-09-18	Remove dead code in dnets.	Pierre-Marie Pédrot
2020-09-16	Merge PR #13008: Use fresher names in eqschemes	Hugo Herbelin
2020-09-13	Statically ensure that only polymophic hint terms come with a context.	Pierre-Marie Pédrot
2020-09-10	Use fresher names in eqschemes.	Jasper Hugunin
2020-09-10	Add a fast-path to Tactics.e_change_in_hyps.	Pierre-Marie Pédrot
2020-09-09	Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...	Pierre-Marie Pédrot
2020-09-08	Merge PR #12993: Remove deprecated tactic cutrewrite.	Clément Pit-Claudel
2020-09-08	Remove deprecated tactic cutrewrite.	Théo Zimmermann
2020-09-08	Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment...	Pierre-Marie Pédrot
2020-09-07	Refine test for unresolved evars: not reachable from initial evars	Matthieu Sozeau
2020-09-06	Merge PR #12976: Remove clenv chaining in Equality	Hugo Herbelin
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	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-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 #12973: Random cleanup around the data structures used in Equality	Hugo Herbelin
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-01	Unify the shelves	Maxime Dénès
2020-08-31	Perform an inversion of control in hint validation for eapply.	Pierre-Marie Pédrot
2020-08-31	Fix mangle names issue in induction	Gaëtan Gilbert
2020-08-31	Fixes a freshness issue with induction (see comment in #12944).	Hugo Herbelin
2020-08-31	Move elim-specific code from Tacticals to Elim.	Pierre-Marie Pédrot
2020-08-28	Clarify variable names in abstract implementation	Gaëtan Gilbert
2020-08-28	Make abstract compatible with mangle names	Gaëtan Gilbert
2020-08-27	Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo	Pierre-Marie Pédrot