aboutsummaryrefslogtreecommitdiff
path: root/pretyping/indrec.ml
AgeCommit message (Expand)Author
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-10Fix constant order in heads.mlMaxime 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
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-07[api] Deprecate `evar_map` ref combinators.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-03Remove unused env argument to fresh_sort_in_familyGaëtan Gilbert
2018-06-13[vernac] Add option to force building really mutual induction schemesMatthieu Sozeau
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Introducing contexts parameterized by the inner term type.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-06Disallow dependent case on prim records w/o etaMatthieu Sozeau
2016-07-06Renaming to more generic has_dependent_elim testMatthieu Sozeau
2016-07-06Move is_prim... to Inductiveops and correct SchemeMatthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Use the canonical name when looking for an eliminator (bug #4670).Guillaume Melquiond
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-15API: documenting context_chop and removing a duplicate.Hugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-11-20Probably useless use of a global-environment reading function in Indrec.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 07:09:31 +0000