diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-16 17:40:04 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2018-03-06 18:24:28 +0100 |
| commit | a768e75f761ae444c05162ec1d064795d413ba25 (patch) | |
| tree | d8d501dda29040c3e750b1077785833675ab3a43 /pretyping/indrec.mli | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
romega: get rid of EConstr.Unsafe
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
Diffstat (limited to 'pretyping/indrec.mli')
0 files changed, 0 insertions, 0 deletions