aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b729f3b9b..5b8eaa50b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -413,7 +413,7 @@ let substl_with_function subst sigma constr =
match v.(i-k-1) with
| (fx, Some (min, ref)) ->
let sigma = Sigma.Unsafe.of_evar_map !evd in
- let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in
+ let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma (EConstr.of_constr dummy) in
let sigma = Sigma.to_evar_map sigma in
evd := sigma;
minargs := Evar.Map.add evk min !minargs;