diff options
| -rw-r--r-- | proofs/clenv.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index e466992721..bb660adf4d 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -128,7 +128,11 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t) +let mk_clenv_type_of gls t = + let env = Proofview.Goal.env gls in + let sigma = Tacmach.New.project gls in + let sigma, tt = Typing.type_of env sigma t in + mk_clenv_from_env env sigma None (t,tt) (******************************************************************) |