diff options
| author | Matthieu Sozeau | 2015-10-04 14:50:45 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-06 10:01:19 +0200 |
| commit | 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f (patch) | |
| tree | 4bb7a90d8474b038434b732fb24b9b9d69e937c3 /tactics/class_tactics.ml | |
| parent | efce61af32ff1b09a21dcf88bca7d6609a0bfd27 (diff) | |
Fix bug #4354: interpret hints in the right env and sigma.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 80f47c680f..ed5b783f6c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -190,7 +190,7 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: + (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (project goal) (pf_concl goal))) in @@ -339,7 +339,7 @@ let make_hints g st only_classes sign = (PathOr (paths, path), hint @ hints) else (paths, hints)) (PathEmpty, []) sign - in Hint_db.add_list hintlist (Hint_db.empty st true) + in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) let make_autogoal_hints = let cache = ref (true, Environ.empty_named_context_val, @@ -374,7 +374,7 @@ let intro_tac : atac = let context = Environ.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) (true,false,false) info.only_classes None (List.hd context) in - let ldb = Hint_db.add_list hint info.hints in + let ldb = Hint_db.add_list env s hint info.hints in (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls in {it = gls'; sigma = s;}) |