aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
authorKenji Maillard2019-11-04 23:44:28 +0100
committerKenji Maillard2019-11-04 23:47:46 +0100
commit5711fc6dcd9a0a566e0bbb543e9d7edb413aacf4 (patch)
tree4452f59bcbc609e2cf0740b3cce3c5b71b7fadeb /interp/implicit_quantifiers.ml
parentf75e1b5d8a4f679c839ffa327baa590198c69640 (diff)
Prevent double definition of Ltac2 constructors inside a module; Fix #11046
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions