diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 2755ed9cb0..4ba9adafec 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1071,7 +1071,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = (* We skip the test whether args is the identity or not *) let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in - if not (Int.Set.is_empty (free_rels t)) then + if not (closed0 c) then error "Hints with holes dependent on a bound variable not supported."; if occur_existential t then (* Not clever enough to construct dependency graph of evars *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index da3ab737b6..1673aac0a5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -558,7 +558,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = ltac_vars = constr_context; ltac_bound = Id.Map.domain ist.lfun; } in - intern_gen kind ~allow_patvar ~ltacvars env c + let kind_for_intern = + match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in + intern_gen kind_for_intern ~allow_patvar ~ltacvars env c in let trace = push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in |