diff options
| author | Pierre-Marie Pédrot | 2015-10-26 15:55:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-26 15:55:15 +0100 |
| commit | aff038fbbe5ade8d58a895b3d2f6e32267c5184c (patch) | |
| tree | 0598bda5a6432894e4fec9ac071cf9ad544d3ee2 /tactics | |
| parent | 010775eba60ea89645792b48a0686ff15c4ebcb5 (diff) | |
| parent | 6417a9e72feb39b87f0b456186100b11d1c87d5f (diff) | |
Merge branch 'v8.5'
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 |