aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun_common.mli
AgeCommit message (Expand)Author
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-09-29Almost fully moving funind to new proof engine.Hugo Herbelin
2020-04-10[ocamlformat] Enable for funind.Emilio Jesus Gallego Arias
2020-02-07Remove unsafe_type_of from funindGaëtan Gilbert
2019-10-25[funind] Removed dead code.Emilio Jesus Gallego Arias
2019-08-29[funind] Don't export duplicate save function.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-07[funind] Move some exception-based control flow to explicit option typing.Emilio Jesus Gallego Arias
2019-08-07[funind] Port indfun 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-31[funind] Move common `make_eq` to funind_common.Emilio Jesus Gallego Arias
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`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-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-03-27[plugins] [funind] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2018-11-30[vernac] [hooks] Refactor towards optional hooks.Emilio Jesus Gallego Arias
2018-11-17[pfedit] Remove cook_proof stub.Emilio Jesus Gallego Arias
2018-11-07[Funind plugin] Remove some dead codeVincent Laporte
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-06-18Remove reference name type.Maxime Dénès
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-06-16Removing Proof_type from the API.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-04-22Merge branch v8.6 into trunkHugo Herbelin
2017-04-04Solving first problem in bug #4306. TO DO : solve the let in problemJulien Forest
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-02-14Funind API using EConstr.Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-04-14Function now supports puniveresjforest
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-10-18declaration_hooks use Ephemerongareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:43:55 +0000