aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
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
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2020-04-10[ocamlformat] Enable for funind.Emilio Jesus Gallego Arias
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-31Merge PR #11915: [proof] Split delayed and regular proof closing functionsPierre-Marie Pédrot
2020-03-31Merge PR #11823: [funind] [cleanup] Remove unused function parametersPierre-Marie Pédrot
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
2020-03-30[declare] Make the type of closed entries opaque.Emilio Jesus Gallego Arias
2020-03-30[ComDefinition] Split program from regular declarationsEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:03:33 +0000