diff options
| author | Matthieu Sozeau | 2015-09-23 16:14:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:10 +0200 |
| commit | 72c6588923dca52be7bc7d750d969ff1baa76c45 (patch) | |
| tree | a8b46ecadae6fcf29b6c3dd504e557dfea444f4e /plugins/cc/cctac.ml | |
| parent | 26628315688e07c43b9881872a737454e93fe4c9 (diff) | |
Univs: fix an evar leak in congruence
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 9c3a0f7299..6439f58d24 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -46,7 +46,7 @@ let whd_delta env= (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c) +let sf_of env sigma c = sort_of env (ref sigma) c let rec decompose_term env sigma t= match kind_of_term (whd env t) with |