diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 10:23:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 15:22:27 +0200 |
| commit | 3806d567af6b1feee2c8f196199eee4208a8551d (patch) | |
| tree | 5e6a7657058d52f18869c3bdfa618e5f7bb26b90 /plugins/cc | |
| parent | f3b714f5a8e516ee9731d705808a4084caae5a1e (diff) | |
Typing.sort_of does not leak evarmaps anymore.
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 1383d8603..e828345fa 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -45,7 +45,8 @@ let whd_delta env= (* decompose member of equality in an applicative format *) -let sf_of env sigma c = family_of_sort (sort_of env sigma c) +(** FIXME: evar leak *) +let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c) let rec decompose_term env sigma t= match kind_of_term (whd env t) with |