diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 15:03:10 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-14 13:25:56 +0200 |
commit | c22ac10752c12bcb23402ad29a73f2d9699248a6 (patch) | |
tree | 9a77251356af06e08c70f46235815f6a6d4c2bfb /tactics/tactics.ml | |
parent | e68f8c904b7ee8fee9f98f75e37ab6d01b54731f (diff) |
Deprecate Typing.e_* functions
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 60070e6fe..01351e249 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1985,24 +1985,22 @@ let on_the_bodies = function exception DependsOnBody of Id.t option let check_is_type env sigma ty = - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - !evdref + let sigma, _ = Typing.sort_of env sigma ty in + sigma with e when CErrors.noncritical e -> raise (DependsOnBody None) let check_decl env sigma decl = let open Context.Named.Declaration in let ty = NamedDecl.get_type decl in - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - let _ = match decl with - | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.e_check env evdref c ty + let sigma, _ = Typing.sort_of env sigma ty in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,c,_) -> Typing.check env sigma c ty in - !evdref + sigma with e when CErrors.noncritical e -> let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) |