aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-27Remove decimal-only number notationsPierre Roux
2021-02-26Signed primitive integersAna
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-18Print primitive constants in debugerPierre Roux
2021-01-12Change the case representation of patterns.Pierre-Marie Pédrot
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-11Removing non relevant argument binding_kind of GLocalDef.Hugo Herbelin
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-11Merge PR #13540: Clean support of primitive integersPierre-Marie Pédrot
2020-12-09Using self-documenting argument names in two exceptions of cases.ml.Hugo Herbelin
2020-12-09Constrintern.ml: some naming uniformity.Hugo Herbelin
2020-12-09Some documentation in constrintern.ml.Hugo Herbelin
2020-12-09Fixing some indentations in constrintern.ml.Hugo Herbelin
2020-12-09Constrintern: Code factorization in interning of record fields.Hugo Herbelin
2020-12-09Constrintern: Grouping together functions about reference locating.Hugo Herbelin
2020-12-09Constrintern cleanup: Centralizing calls to find_appl_head.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-12-09Move addition of parameters in asymmetric mode to first phase of pat interning.Hugo Herbelin
2020-12-09Removing a useless explicit use of subscopes in interpreting arguments of a n...Hugo Herbelin
2020-12-09Constrintern: As in terms, accept @C for C abbreviation in cases patterns.Hugo Herbelin
2020-12-09Constrintern: shortcut in cases pattern interning.Hugo Herbelin
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-12-02Greatly simplify the conversion functions between Z.t and Uint63.t.Guillaume Melquiond
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-24Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ...coqbot-app[bot]
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.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-20Rewriting convoluted code of set_var_scope in constrintern.ml.Hugo Herbelin
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized 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-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
2020-11-17A reimport of notations now put the corresponding notations again in front.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Fixing alpha-equality of notation interpretations with recursive patterns.Hugo Herbelin
2020-11-16Using labels to document match_notation_constr.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:43:38 +0000