aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun.ml
AgeCommit message (Expand)Author
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.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 principle generation to its own file.Emilio Jesus Gallego Arias
2019-07-31[funind] Derive_correctness is only used in funind, thus more there.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
2019-07-15[funind] Remove unneeded callback.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[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-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
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[vernac] more precise types for Add Morph, Instance, and FunctionEnrico Tassi
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-04Funind: use maybe_open_proof a bit lessGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:42:33 +0000