aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.mli
AgeCommit message (Expand)Author
2021-02-17Use make_case_or_project in auto_ind_declGaëtan Gilbert
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-11-04Further code simplification in arbitrary hint interpretation.Pierre-Marie Pédrot
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2019-01-21[EConstr] Expose API to normalize and check if evars are remainingMaxime Dénès
2018-10-28[error printing] Fix improper grounding of open terms in printing.Emilio Jesus Gallego Arias
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-09-03Adding combinators preserving expanded form of branches and pred. of "match".Hugo Herbelin
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-06-08Add a bit of doc to EConstr.decompose_lam*Gaëtan Gilbert
2018-05-17Split off Universes functions about substitutions and constraintsGaë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-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Pierre-Marie Pédrot
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Option for messing with inference of irrelevant constraintsGaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-27Add a comment on EConstr.to_constr regarding evar-freeness.Pierre-Marie Pédrot
2018-01-19Define EConstr version of [push_rec_types].Cyprien Mangin
2017-12-13[econstr] Add a couple of new API functions.Emilio Jesus Gallego Arias
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
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-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:54:26 +0000