aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre Letouzey2017-06-16 17:40:04 +0200
committerPierre Letouzey2018-03-06 18:24:28 +0100
commita768e75f761ae444c05162ec1d064795d413ba25 (patch)
treed8d501dda29040c3e750b1077785833675ab3a43 /dev
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (diff)
romega: get rid of EConstr.Unsafe
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions