coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-16	Avoid exposing an internal names when "intros _ H" fails.	Hugo Herbelin
2020-11-16	Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"	coqbot-app[bot]
2020-11-15	Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"	Jim Fehrle
2020-11-15	Implement export locality for the remaining Hint commands.	Pierre-Marie Pédrot
2020-11-12	Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...	Pierre-Marie Pédrot
2020-11-04	Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.	Hugo Herbelin
2020-11-04	Do not try to be clever for term-as-hint interpretation.	Pierre-Marie Pédrot
2020-11-04	Opacify the Hints.hint_term type.	Pierre-Marie Pédrot
2020-11-04	Encapsulate the last use of IsConstr in the Hints API.	Pierre-Marie Pédrot
2020-11-04	Further API cleanup after the removal of forward hints.	Pierre-Marie Pédrot
2020-10-21	Add missing deprecations in Projection API.	Pierre-Marie Pédrot
2020-10-21	Similar introduction of a Construct module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Introduce an Ind module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Rename the GlobRef comparison modules following the standard pattern.	Pierre-Marie Pédrot
2020-10-21	Same little game with Projection.	Pierre-Marie Pédrot
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
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