aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-01Fix a bug in funind.Pierre-Marie Pédrot
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-29Applying ocamlformat.Hugo Herbelin
2020-09-29Almost fully moving funind to new proof engine.Hugo Herbelin
2020-08-25funind: stop using intro_usingGaëtan Gilbert
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-26[declare] Return list of declared global in Proof.saveEmilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] Move udecl to Info structure.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove Lemmas moduleEmilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-09Merge PR #12241: [declare] Merge DeclareDef into DeclareGaëtan Gilbert
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-07Remove call to Refiner API from Funind.Pierre-Marie Pédrot
2020-05-07Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.Gaëtan Gilbert
2020-05-03[declare] Add deprecation notices for compat modules.Emilio Jesus Gallego Arias
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
2020-05-03[funind] Make `build_functional_principle` use a functional evar_mapEmilio Jesus Gallego Arias
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-05-01Warn when a (co)fixpoint is not truly recursive.Hugo Herbelin
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables (incid...Lysxia
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15Merge PR #11776: [ocamlformat] Enable for funind.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:22:24 +0000