aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Expand)Author
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-02-26Signed primitive integersAna
2021-01-12Change the case representation of patterns.Pierre-Marie Pédrot
2020-12-11Removing non relevant argument binding_kind of GLocalDef.Hugo Herbelin
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.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-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-10-30Renaming Numeral into NumberPierre Roux
2020-10-20Merge PR #13180: Respect Print Universes when printing primitive arrayscoqbot-app[bot]
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing tim...Pierre-Marie Pédrot
2020-10-12Respect Print Universes when printing primitive arraysGaëtan Gilbert
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were miss...Hugo Herbelin
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-25Dead code in adjust_implicit_arguments.Hugo Herbelin
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...Emilio Jesus Gallego Arias
2020-05-14Fixes #12322 (anomaly when printing "fun" binders with implicit types).Hugo Herbelin
2020-05-09Add hexadecimal numeralsPierre Roux
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ...Hugo Herbelin
2020-04-11Renaming confusingly-named insert_coercion into insert_entry_coercion.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-23Not iterating recursive notations more than once.Hugo Herbelin
2020-02-23parens --> parenthesesAbhishek Anand (optiplex7010@home)
2020-02-23added the new optionAbhishek Anand (optiplex7010@home)
2020-02-22In printing patterns, distinguish the case of a notation to @id.Hugo Herbelin
2020-02-22Fix index bug in computing implicit signature of abbrev. in pattern printing.Hugo Herbelin
2020-02-22Fix inheritance of argument scopes when printing notations in patterns.Hugo Herbelin
2020-02-22Use auxiliary function for externing record patterns.Hugo Herbelin
2020-02-22Inherit argument scopes in notations to expressions of the form @f.Hugo Herbelin
2020-02-22Deactivate implicit arguments in printing notations bound to "@f".Hugo Herbelin
2020-02-22Fixing printing of notations bound to an expression of the form "@f".Hugo Herbelin
2020-02-22Fixing a notation printing bug (missing a @ to reflect absence of imp. args).Hugo Herbelin
2020-02-22Fixing anomaly from #11091 (incompatible printing with notation and imp. args).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:54:23 +0000