aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
AgeCommit message (Expand)Author
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
2020-09-02Fixes #9403 and #10803 (missing flattening of nested applications in notations).Hugo Herbelin
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-23Not iterating recursive notations more than once.Hugo Herbelin
2020-02-22In printing patterns, distinguish the case of a notation to @id.Hugo Herbelin
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env in Glob_opsMaxime Dénès
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2019-02-04Primitive integersMaxime Dénès
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-10-23Fixing #8794 (anomaly with abbreviation involving both term and binders).Hugo Herbelin
2018-10-08Fixes #8672 (ill-formed pattern substitution in notation with "let").Hugo Herbelin
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-13Fixing a bug in printing the body of a located notation.Hugo Herbelin
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-03-29Fixes #7110 ("as" untested while looking for notation for nested patterns).Hugo Herbelin
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-23Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Hugo Herbelin
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20When printing a notation with "match", more flexibility in matching equations.Hugo Herbelin
2018-02-20Adding general support for irrefutable disjunctive patterns.Hugo Herbelin
2018-02-20Using an "as" clause when needed for printing irrefutable patterns.Hugo Herbelin
2018-02-20Refining the strategy for glueing let-ins to a sequence of binders.Hugo Herbelin
2018-02-20A (significant) simplification in printing notations with recursive binders.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:08:33 +0000