aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
AgeCommit message (Expand)Author
2020-07-02Fix record pattern interpretation with implicit argumentsGaëtan Gilbert
2020-05-15[interp] Register printers for InternalizationError instead of ad-hoc hanlding.Emilio Jesus Gallego Arias
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
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-13Close #11935: section variables do not have universe instances.Gaë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-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-25Fixing residual bug of #11120.Hugo Herbelin
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-22Inherit scopes and implicit sign. in notations for partially applied pattern.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-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
2020-02-11Reinforcing the role of type "typing_constraint".Hugo Herbelin
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-01-30Minor indentation change.Hugo Herbelin
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
2019-12-04Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.Hugo Herbelin
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
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-07-03Move variable_secpath logic to dumpglob from constrinternGaëtan Gilbert
2019-07-03Remove constrintern global_level dead codeGaëtan Gilbert
2019-06-18Merge PR #10199: Fix computation of implicit arguments when names collide in ...Maxime Dénès
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Merge PR #10226: Simplify implicit_quantifiersEmilio Jesus Gallego Arias
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-06-11Simplify implicit_quantifiersGaëtan Gilbert
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Fixing typos - Part 2JPR
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:21 +0000