aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.ml
AgeCommit message (Expand)Author
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
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.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-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-08Normalizing universes before performing term comparison.Pierre-Marie Pédrot
2017-09-08Using EConstr equality check in unification.Pierre-Marie Pédrot
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
2017-05-31Using EConstr and more invariants in record.ml.Hugo Herbelin
2017-05-29tactics cleanup: remove constr_of_global callsMatthieu Sozeau
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-19Exporting some functions of vars.ml as functions operating on EConstr.Hugo Herbelin
2017-05-19In EConstr, defining some "cast" functions earlier.Hugo Herbelin
2017-05-19Moving "sym" on "eq" type to lib/util.ml.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:29:33 +0000