aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 17:14:54 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 17:14:54 +0100
commit3875a525ee1e075be9f0eb1f17c74726e9f38b43 (patch)
treef64a545676d221ee1279dfa92903d44d0509196b /pretyping
parente9d2a40ed12e31095565b5c7401f02af997a7cc7 (diff)
parenta768e75f761ae444c05162ec1d064795d413ba25 (diff)
Merge PR #6918: romega: get rid of EConstr.Unsafe
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions