aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-10-27 13:31:44 +0100
committerPierre-Marie Pédrot2020-10-27 13:31:44 +0100
commitb87fd6cfe5fe872a38d98c294aea84cde8c6c160 (patch)
tree060327d404f1e9fcf198aff8d5f075ec498f261e /kernel/nativelambda.ml
parent82f7cc4a408cf100fda43139c0b1d33e33748799 (diff)
parent30f97beb1bfc149d9608cb74f24f69f268671e04 (diff)
Merge PR #13167: Ltac2: use ComTactic infrastructure
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions