diff options
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 572fa32b7..6c59abe66 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -785,6 +785,7 @@ let interp_may_eval f ist env sigma = function let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma (EConstr.of_constr c_interp) in + let c = EConstr.Unsafe.to_constr c in (Sigma.to_evar_map sigma, c) | ConstrContext ((loc,s),c) -> (try |