diff options
| author | Gaëtan Gilbert | 2020-02-06 15:48:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 8a736c4d3aaf941416ffc616c296a3b077d6242f (patch) | |
| tree | 0745a764fb35eedaa8cfe6a384143ea66bb8d548 | |
| parent | dd4c9f7218f3d4fd883c0ae73cd41cd12049e86e (diff) | |
unsafe_type_of -> type_of in Tactics.guess_elim
| -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 f5685e07af..1624c4a62d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4231,8 +4231,8 @@ let guess_elim isrec dep s hyp0 gl = let ind = EConstr.of_constr ind in (sigma, ind) in - let elimt = Typing.unsafe_type_of env sigma elimc in - sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) + let sigma, elimt = Typing.type_of env sigma elimc in + sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) let given_elim hyp0 (elimc,lbind as e) gl = let sigma = Tacmach.New.project gl in |