diff options
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 79b5c1622..6a04badf3 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -584,7 +584,7 @@ let interp_glob_closure ist env sigma ?(kind=WithoutTypeConstraint) ?(pattern_mo ltac_bound = Id.Map.domain ist.lfun; ltac_extra = Genintern.Store.empty; } in - { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env term_expr } + { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env sigma term_expr } let interp_uconstr ist env sigma c = interp_glob_closure ist env sigma c |