diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
| commit | a40fb961c8ffeeb03769404cacda8bd6cff17417 (patch) | |
| tree | 7105d621bc16f825c1f309e3d5b7720b1b1513ec /plugins/ssr/ssrequality.ml | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
| parent | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (diff) | |
Merge PR #6893: Cleanup UState API usage
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 859513d5c..57635edac 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -216,7 +216,7 @@ let same_proj sigma t1 t2 = let all_ok _ _ = true let fake_pmatcher_end () = - mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp) + mkProp, L2R, (Evd.empty, UState.empty, mkProp) let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in |