aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-10 17:23:32 +0000
committerGitHub2020-12-10 17:23:32 +0000
commit71031ef2a7032bccb55cc0e6035900c5b843583c (patch)
tree3e568d98c1ccea2e2e5c9ab055c2163d9291db72 /doc/plugin_tutorial
parentc3ba8edf47e9afd1d2d226c2d006bbc7830b254a (diff)
parentdc7a4f056d97c43badaa6ca5901eafb951527d88 (diff)
Merge PR #12100: Fixing use of argument scopes in patterns + a further cleanup of constrintern.ml
Reviewed-by: SkySkimmer Ack-by: ppedrot
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions