diff options
| author | Gaëtan Gilbert | 2020-02-06 16:40:15 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 1c1eed73491ea84ee58eec703fbeedf9667a06ef (patch) | |
| tree | 5991696e3c93a734ab5ca8317ef0ea2322a50f03 | |
| parent | 63883d37318fa54101b3ec4029cb26f0ae8439a3 (diff) | |
unsafe_type_of -> get_type_of in Inv.raw_inversion
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index be0421d42d..2181eb25af 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -464,7 +464,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c) with UserError _ -> let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in CErrors.user_err msg |