diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-31 10:59:24 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-31 10:59:24 +0200 |
commit | ac8a84e3b4dc530b000e17b72c7e26f7a957420f (patch) | |
tree | baf58d74b6629034cecb577eade044f29313cc4d /tactics/tactics.ml | |
parent | 22db6304ffd45d7ae6e4a0acf909afb1ec55d02c (diff) | |
parent | 0dc79e09b2b7c369b35191191aa257451a536540 (diff) |
Merge PR #6969: [api] Remove functions deprecated in 8.8
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bb57e2bf4..58c62af85 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1910,8 +1910,8 @@ let cast_no_check cast c = exact_no_check (mkCast (c, cast, concl)) end -let vm_cast_no_check c = cast_no_check Term.VMcast c -let native_cast_no_check c = cast_no_check Term.NATIVEcast c +let vm_cast_no_check c = cast_no_check VMcast c +let native_cast_no_check c = cast_no_check NATIVEcast c let exact_proof c = let open Tacmach.New in |