aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-03-11 10:02:17 +0100
committerPierre-Marie Pédrot2020-03-11 10:02:17 +0100
commit45e83041ee129a541fdf17a8c50dd6e9e0e81262 (patch)
tree27ce0770df7c30aca0225ce5a9fbff02b508b288 /kernel/constr.ml
parentbaae1974d5ee15233cddffa1281d4a23fc74cc9f (diff)
parent15eb6b5721aaff1281f1f71e00c98fd9a39511e0 (diff)
Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constants
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions