diff options
| author | Matthieu Sozeau | 2016-06-29 11:55:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-29 11:55:31 +0200 |
| commit | 5e979cf6020eea9fa0feaa77c7436a29443e35db (patch) | |
| tree | 7f2d28d1bfb9dfb72788b434ecada5603afecb57 /engine/evd.ml | |
| parent | 58b6784fee71a16719bc4f268dc42830c06a5c63 (diff) | |
| parent | 40ee96a0392fbc0945c48b5b134aa1be36f86225 (diff) | |
Merge branch 'bug4527' into trunk
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index b883db615e..1276c5994e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -252,6 +252,7 @@ let instantiate_evar_array info c args = | _ -> replace_vars inst c type evar_universe_context = UState.t + type 'a in_evar_universe_context = 'a * evar_universe_context let empty_evar_universe_context = UState.empty |