aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
2020-04-30Move availability_of_prim_tokenPierre Roux
2020-04-29Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ...Emilio Jesus Gallego Arias
2020-04-22Merge PR #11694: Support printing argument-free abbreviations in custom entri...Emilio Jesus Gallego Arias
2020-04-21Fixing #3451: coqdoc links for projections of tuples rather than for construc...Hugo Herbelin
2020-04-21Constrintern: another reworking of the interning of records.Hugo Herbelin
2020-04-21Constrintern.ml: simplifying the interning of record tuples.Hugo Herbelin
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
2020-04-15Making type interning_data abstract in constrintern.ml.Hugo Herbelin
2020-04-15Small convenient code factorization in constrintern.ml.Hugo Herbelin
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
2020-04-14Merge PR #11978: Close #11935: section variables do not have universe instances.Pierre-Marie Pédrot
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-04-13correctly open objects for Names filtersGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
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-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
2020-03-31Remove check_hidden_implicit_parameters (not needed anymore)Gaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-22Adding support for parsing "+" sig in NumTok.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-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-25Fixing residual bug of #11120.Hugo Herbelin
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-22Fixes #4690: do not allow @f in notations when f is a notation variable.Hugo Herbelin
2020-02-22Inherit arguments scopes in pattern notations bound to some @id.Hugo Herbelin
2020-02-22In printing patterns, distinguish the case of a notation to @id.Hugo Herbelin
2020-02-22Inherit scopes and implicit sign. in notations for partially applied pattern.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-22Propagate implicit arguments in all notations for partial applications.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
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:53:03 +0000