aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun.ml
AgeCommit message (Expand)Author
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-03-27[plugins] [funind] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2018-11-30[vernac] [hooks] Refactor towards optional hooks.Emilio Jesus Gallego Arias
2018-11-02Remove is_universe_polymorphism in funindGaëtan Gilbert
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-23[api] Deprecate constructors of deprecated datatypes.Emilio Jesus Gallego Arias
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-11Correction of ugly message described in #4667Julien Forest
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-01-24Remove dead code from funind.Maxime Dénès
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-01Detyping functions are now operating on EConstr.t.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-23closing bug #4250Julien Forest
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-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-31Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:41:00 +0000