aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
AgeCommit message (Expand)Author
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2020-12-11Removing non relevant argument binding_kind of GLocalDef.Hugo Herbelin
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-20Enforcing when a binding variable has no explicit type in constr_notation.Hugo Herbelin
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ...coqbot-app[bot]
2020-11-18In recursive notations, accept partial application over the recursive pattern.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
2020-11-16Fixing alpha-equality of notation interpretations with recursive patterns.Hugo Herbelin
2020-11-16Using labels to document match_notation_constr.Hugo Herbelin
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
2020-11-05Accept section variables in notations with mixed terms and binders.Hugo Herbelin
2020-11-05Notations: Giving a consistent role to global references occurring patterns.Hugo Herbelin
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding not...coqbot-app[bot]
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-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:40:08 +0000