aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.ml
AgeCommit message (Expand)Author
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-02Move *_with_full_binders variants out of the kernel.Pierre-Marie Pédrot
2020-10-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
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-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
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-03-11Comment difference between the 2 hashes on constrGaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
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-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-16Fix lifting in foo_with_full_binders for (co)fixpointsGaëtan Gilbert
2018-11-16Small simplification in fold_constr_with_bindersGaëtan Gilbert
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-10-26Merge PR #7186: Moving `fold_constr_with_full_binders` to a placeMaxime Dénès
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-16Simplify fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-10-12Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.Hugo Herbelin
2018-09-28Generalize type of compare_head_with functionsGaëtan Gilbert
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
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-26Remove Sorts.contentsGaëtan Gilbert
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
2018-06-05Define rec_declaration in terms of prec_declaration.SimonBoulier
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime 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-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-01-26Safer VM interfacesMaxime Dénès
2017-11-24Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Maxime Dénès
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio 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-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:03:57 +0000