diff options
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 6c59abe66..b4d2b1e50 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -802,7 +802,8 @@ let interp_may_eval f ist env sigma = function (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) + let (sigma, t) = Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) in + (sigma, EConstr.Unsafe.to_constr t) | ConstrTerm c -> try f ist env sigma c |