diff options
| -rw-r--r-- | contrib/cc/cctac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index 2509dffd5c..84388b1c09 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -58,7 +58,7 @@ let whd_delta env= (* decompose member of equality in an applicative format *) -let sf_of env sigma c = family_of_sort (destSort (whd_delta env (type_of env sigma c))) +let sf_of env sigma c = family_of_sort (sort_of env sigma c) let rec decompose_term env sigma t= match kind_of_term (whd env t) with |