aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-01-26 11:08:28 +0000
committerGitHub2021-01-26 11:08:28 +0000
commit1a84bed789697ff9b4f5c70dec3c732cdbbdbce0 (patch)
tree85cbefe72ebbeaa9b3d6c1c27545864f96faa245 /kernel/nativelambda.ml
parent14051337936db1f56dc052a6e54e5b606552141b (diff)
parent7ea0db435910c2db2a9ae4cadfd54f49f3640b62 (diff)
Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions