aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/pretyping.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8baa668c7b..5e6a3eac73 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1126,7 +1126,7 @@ let type_uconstr ?(flags = constr_flags)
ltac_constrs = closure.typed;
ltac_uconstrs = closure.untyped;
ltac_idents = closure.idents;
- ltac_genargs = ist.Geninterp.lfun;
+ ltac_genargs = Id.Map.empty;
} in
let sigma = Sigma.to_evar_map sigma in
let (sigma, c) = understand_ltac flags env sigma vars expected_type term in