From 1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 13:31:54 +0100 Subject: Renaming functions in Typing to stick to the standard e_* scheme. --- plugins/cc/cctac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 09d9cf019..bea449c31 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -47,7 +47,7 @@ let whd_delta env= (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = sort_of env (ref sigma) c +let sf_of env sigma c = e_sort_of env (ref sigma) c let rec decompose_term env sigma t= match kind_of_term (whd env t) with -- cgit v1.2.3