aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
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
2020-03-30[proof] Miscellaneous cleanup on proof info handlingEmilio Jesus Gallego Arias
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
2020-03-13[funind] [cleanup] Remove unused function parametersEmilio Jesus Gallego Arias
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-07Remove unsafe_type_of from funindGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
2020-02-07Remove confusing commented code in funindGaëtan Gilbert
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
2019-10-25[funind] Removed dead code.Emilio Jesus Gallego Arias
2019-09-29Merge PR #10673: [lemmas] Cleanup users of default proof information.Pierre-Marie Pédrot
2019-08-29[funind] Don't export duplicate save function.Emilio Jesus Gallego Arias
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ...Pierre-Marie Pédrot
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
2019-08-27Merge PR #10635: [funind] Port indfun to the new tactic engine.Pierre-Marie Pédrot
2019-08-23[lemmas] Cleanup users of default proof information.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:45:03 +0000