aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-06-16 17:40:04 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2018-03-06 18:24:28 +0100
commita768e75f761ae444c05162ec1d064795d413ba25 (patch)
treed8d501dda29040c3e750b1077785833675ab3a43 /plugins/ssr
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (diff)
romega: get rid of EConstr.Unsafe
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
Diffstat (limited to 'plugins/ssr')
0 files changed, 0 insertions, 0 deletions