diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index efc2a9b822..05b26cbb64 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -348,7 +348,7 @@ let glob_quantified_hypothesis ist x = let glob_constr ist c = let _ = - Constrintern.interp_rawconstr_gen + Constrintern.interp_rawconstr_gen false Evd.empty (Global.env()) [] false (fst ist) c in c |