diff options
Diffstat (limited to 'tactics')
| -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 |