From c22ac10752c12bcb23402ad29a73f2d9699248a6 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 26 Apr 2018 15:03:10 +0200 Subject: Deprecate Typing.e_* functions --- plugins/cc/cctac.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c4db49cd3..361981c5b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -49,7 +49,7 @@ let whd_delta env sigma t = (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = e_sort_of env (ref sigma) c +let sf_of env sigma c = snd (sort_of env sigma c) let rec decompose_term env sigma t= match EConstr.kind sigma (whd env sigma t) with @@ -264,9 +264,8 @@ let app_global_with_holes f args n = let ans = mkApp (fc, args) in let (sigma, holes) = gen_holes env sigma t n [] in let ans = applist (ans, holes) in - let evdref = ref sigma in - let () = Typing.e_check env evdref ans concl in - (!evdref, ans) + let sigma = Typing.check env sigma ans concl in + (sigma, ans) end end -- cgit v1.2.3