aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.mli
AgeCommit message (Expand)Author
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-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-28Generalize type of compare_head_with functionsGaëtan Gilbert
2018-09-17Merge PR #8053: [dune] Add apidoc target using `odoc`Gaëtan Gilbert
2018-09-12Fix mli-doc following #7109.Théo Zimmermann
2018-09-10[dune] Add apidoc target using `odoc`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-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-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-12-19Fix order of let-in representation comment.Jasper Hugunin
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
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-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-01More consistent writing of de Bruijn.Théo Zimmermann
2017-05-01Fix for bug 5507. Mispelt de Bruijn.Théo Zimmermann
2017-03-31Make the Constr.kind_of_term type parametric in sorts and universes.Pierre-Marie Pédrot
2016-11-08Introducing a new EConstr.t type to perform the nf_evar operation on demand.Pierre-Marie Pédrot
2016-10-26COMMENT: Constr.kind_of_termMatej Kosik
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11COMMENTS: of "Constr.case_info" type were updated.Matej Kosik
2015-12-18COMMENTS: added to the "Constr.case_info" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of the "Constr.kind_of_term" type.Matej Kosik
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-02-24New function [Constr.equal_with] to compare terms up to variants of [kind_of_...Arnaud Spiwack
2015-02-24Refactoring in [Constr].Arnaud Spiwack
2015-01-12Update headers.Maxime Dénès
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-05-26Update infer_conv to record trivial Prop <= Type i constraints that are neede...Matthieu Sozeau
2014-05-06Add doc on the new API for universe polymorphism and primitive projectionsMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-04-24Adding a [fold_map] operation on constrs.Pierre-Marie Pédrot
2014-03-03Removing generic hashes in kernel.Pierre-Marie Pédrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:03:57 +0000