aboutsummaryrefslogtreecommitdiff
path: root/tactics/inv.ml
AgeCommit message (Expand)Author
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
2020-09-04Statically enforce that elim is passed a fully applied inductive type.Pierre-Marie Pédrot
2020-09-04Enforce the argument of elim functions to be a variable.Pierre-Marie Pédrot
2020-09-02Factorize the only uses of internal API in Elim for Inv.Pierre-Marie Pédrot
2020-09-02Further remove the type Elim.branch_assumptions.Pierre-Marie Pédrot
2020-08-31Move elim-specific code from Tacticals to Elim.Pierre-Marie Pédrot
2020-08-18Tactic inversion: adding support for registration of an equality in Type.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Inv.raw_inversionGaë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-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-07[api] Deprecate `evar_map` ref combinators.Emilio Jesus Gallego Arias
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
2018-07-03Remove unused env argument to fresh_sort_in_familyGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
2018-06-04Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Matthieu Sozeau
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-10Replace uses of Termops.dependent by more specific functions.Pierre-Marie Pédrot
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2017-12-07Getting rid of pf_matches in Hipattern.Pierre-Marie Pédrot
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-13Explicit the unsafe flag of all calls to Refine.refine.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Proofview.Goal primitive now return EConstrs.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:36:42 +0000