aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.ml
AgeCommit message (Expand)Author
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-04Further code simplification in arbitrary hint interpretation.Pierre-Marie Pédrot
2020-11-02Merge PR #13273: universes_of_constr: don't ignore CaseInvert universesPierre-Marie Pédrot
2020-10-26universes_of_constr: don't ignore CaseInvert universesGaëtan Gilbert
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.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-04-06Use lists instead of arrays in evar instances.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-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
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-03-14Make Sorts.t privateGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-16Share open recursor code between econstr and constrGaëtan Gilbert
2018-11-16Fix lifting in foo_with_full_binders for (co)fixpointsGaëtan Gilbert
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-28Cleanup comparisons in econstr (compare_head_... users)Gaëtan Gilbert
2018-09-23Fix #8513: EConstr.eq_constr doesn't properly take into account universe vari...Pierre-Marie Pédrot
2018-09-03Adding combinators preserving expanded form of branches and pred. of "match".Hugo Herbelin
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
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-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-09Adjust EConstr.cmp_constructors for relaxed constructor cumulativityGaëtan Gilbert
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Statically enforce that ULub is only between levels.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-02-27Update headers following #6543.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:37:54 +0000