aboutsummaryrefslogtreecommitdiff
path: root/tactics/elim.ml
AgeCommit message (Expand)Author
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-06unsafe_type_of -> get_type_of in Elim.induction_trailerGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Elim.general_decomposer + pf_apply in ifOnHypGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Elim API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacticals API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Fixing some problems with double induction.Hugo Herbelin
2016-01-20Code simplification in elim.ml.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-14Moving is_quantified_hypothesis to new proof engine.Hugo Herbelin
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-22Removing tactic compatibility layer from Elim.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
2014-03-28Define Tactics.bring_hyps in the new monad.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Fixing pervasive equalities. In particular, I removed the code that deletedPierre-Marie Pédrot
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 12:21:29 +0000