From adc507a2a6dc19b34b1d3906bc4c157fb47bb547 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 14 Sep 2008 10:07:44 +0000 Subject: Fix bug #1939: defined evars were not substituted in some typeclasses eauto goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11404 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/class_tactics.ml4 | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index ba090c533..2d4f6715e 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -209,8 +209,8 @@ module SearchProblem = struct prlist (pr_ev evars) (sig_it gls) let filter_tactics (glls,v) l = -(* let glls,nv = apply_tac_list tclNORMEVAR glls in *) -(* let v p = v (nv p) in *) + let glls,nv = apply_tac_list Refiner.tclNORMEVAR glls in + let v p = v (nv p) in let rec aux = function | [] -> [] | (tac,pri,pptac) :: tacl -> @@ -251,9 +251,11 @@ module SearchProblem = struct Option.iter (fun r -> (* msg (str"do cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *) r := true) do_cut; + let sigma = Evarutil.nf_evars sigma in let gl = List.map (Evarutil.nf_evar_info sigma) gl in let nbgl = List.length gl in - let g = { it = List.hd gl ; sigma = sigma } in +(* let gl' = { it = gl ; sigma = sigma } in *) +(* let tacres' = gl', snd s.tacres in *) let new_db, localdb = let tl = List.tl s.localdb in match tl with @@ -295,10 +297,9 @@ module SearchProblem = struct last_tactic = pp; pri = pri; localdb = list_tabulate (fun _ -> new_db) (nbgl'-nbgl) @ localdb } in - let concl = Evarutil.nf_evar (project g) (pf_concl g) in let rec_tacs = let l = - filter_tactics s.tacres (e_possible_resolve s.dblist ldb concl) + filter_tactics s.tacres (e_possible_resolve s.dblist ldb (List.hd gl).evar_concl) in List.map possible_resolve l in -- cgit v1.2.3