aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.mli
AgeCommit message (Expand)Author
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2018-06-12[api] Misctypes removal: tactic flags.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: multi to tactics/rewriteEmilio Jesus Gallego Arias
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-07-31Correcting [build_discriminator] to make the test-suite passamblaf
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-29Equality cleanup: remove constr_of_globalMatthieu Sozeau
2017-05-17Stopping injection not to work on discriminable atoms (see #4890).Hugo Herbelin
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-02-14Equality 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
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-03-05Exporting build_selector, a component of discriminate, for use in congruence.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-10-13Fix some typos.Guillaume Melquiond
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo 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-03-26Removing tactic compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Clean up a warning.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:41:47 +0000