coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-20	Remove double induction tactic	Jim Fehrle
2020-10-21	Introduce an Ind module in the Names API.	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-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	Further remove the type Elim.branch_assumptions.	Pierre-Marie Pédrot
2020-08-31	Move elim-specific code from Tacticals to Elim.	Pierre-Marie Pédrot
2020-08-25	elim.ml: stop using intro_using	Gaëtan Gilbert
2020-05-14	[exn] [tactics] improve backtraces on monadic errors	Emilio Jesus Gallego Arias
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-06	unsafe_type_of -> get_type_of in Elim.induction_trailer	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> get_type_of in Elim.general_decomposer + pf_apply in ifOnHyp	Gaëtan Gilbert
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-04-10	Remove calls to global env in Inductiveops	Maxime Dénès
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-06	Remove the Sigma (monotonous state) API.	Maxime Dénès
2017-04-27	Remove unused [open] statements	Gaetan Gilbert
2017-02-14	Removing most nf_enter in tactics.	Pierre-Marie Pédrot
2017-02-14	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot
2017-02-14	Elim API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Tactics API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Hipattern API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Tacticals API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Tacmach API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Reductionops API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Termops API using EConstr.	Pierre-Marie Pédrot
2016-08-24	CLEANUP: minor readability improvements	Matej Kosik
2016-06-18	Adding eintros to respect the e- prefix policy.	Hugo Herbelin
2016-05-16	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot
2016-05-16	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot
2016-02-09	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-21	Fixing some problems with double induction.	Hugo Herbelin
2016-01-20	Code simplification in elim.ml.	Hugo Herbelin
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-14	Moving is_quantified_hypothesis to new proof engine.	Hugo Herbelin
2015-10-20	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot
2015-10-20	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot
2015-05-13	Safer typing primitives.	Pierre-Marie Pédrot
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-12-09	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin