diff options
| author | Gaëtan Gilbert | 2020-02-06 15:39:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 3faf22b382379f08d5a918bd535287f57e2fc0fc (patch) | |
| tree | 86c9800550b752396a4532c23b3120118dc3bdb0 | |
| parent | e12cfbafbce3a1c6719d7e4d34fe64a81cce90b2 (diff) | |
unsafe_type_of -> get_type_of in Tactics.atomize_param_of_ind_then
Not 100% sure about this one TBH, this function is messy.
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 87389f0be0..da798dd2ce 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3399,8 +3399,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match EConstr.kind sigma c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar env sigma (type_of c) Anonymous in + let type_of = Tacmach.New.pf_get_type_of gl in + id_of_name_using_hdchar env sigma (type_of c) Anonymous + in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) |