aboutsummaryrefslogtreecommitdiff
path: root/pretyping/recordops.mli
AgeCommit message (Expand)Author
2020-11-19Use a proper canonical structure entry for projections.Hugo Herbelin
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-09Fix build after merge of #11164Gaëtan Gilbert
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-10[Canonical structures] “not_canonical” annotation to field declarationsVincent Laporte
2019-05-10[Canonical structures] Some projections may not be canonicalVincent Laporte
2019-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-30[Canonical structures] Minor refactoringVincent Laporte
2018-11-16No Projection.constant in projection <-> constant declarationGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
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-10-17Properly handling projection parameters in canonical structures.Pierre-Marie Pédrot
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-13Getting rid of AUContext abstraction breakers in Recordops.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-02-14Recordops API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-15Documenting check_record + changing a possibly undefined int into int option.Hugo Herbelin
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2013-09-12Unplugging Autoinstance. The code is still here if someone wishesppedrot
2013-08-22Misc changes around coqtop.ml :letouzey
2012-12-18Modulification of nameppedrot
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-26Misc small fixes : warning, dep cycles, ocamlbuild...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:30:40 +0000