aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/recdef.ml
AgeCommit message (Expand)Author
2020-07-01UIP in SPropGaëtan Gilbert
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-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-05-07Remove call to Refiner API from Funind.Pierre-Marie Pédrot
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-10[ocamlformat] Enable for funind.Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2020-02-07Remove unsafe_type_of from funindGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-25[funind] Removed dead code.Emilio Jesus Gallego Arias
2019-08-23[lemmas] Cleanup users of default proof information.Emilio Jesus Gallego Arias
2019-07-31[funind] Port aux function to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-31[funind] Move duplicated `observe_tac` function to indfun_common.Emilio Jesus Gallego Arias
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-09[proof] Remove sign parameter to open_lemma.Emilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-28Merge PR #10434: [declare] Fine tuning of Hook type.Pierre-Marie Pédrot
2019-06-26[stm] [vernac] Remove special ?proof parameter from vernac main pathEmilio Jesus Gallego Arias
2019-06-26[declare] Fine tuning of Hook type.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
2019-06-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-12[funind] Untabify; necessary to ease the review of subsequent work.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-23Fixing typos - Part 2JPR
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 23:08:02 +0000