From 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 9 Jul 2009 15:32:28 +0000 Subject: Use the proper unification flags in e_exact. This makes exact fail a bit more often but respects the spec better. The changes in the stdlib are reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing conversion with delta on open terms in that case). Also fix a minor bug in typeclasses not seeing typeclass evars when their type was a (defined) evar itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/interface/blast.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/interface/blast.ml b/plugins/interface/blast.ml index 57b4d1af8..2f0095a56 100644 --- a/plugins/interface/blast.ml +++ b/plugins/interface/blast.ml @@ -187,7 +187,7 @@ and e_my_find_search db_list local_db hdc concl = match t with | Res_pf (term,cl) -> unify_resolve st (term,cl) | ERes_pf (term,cl) -> unify_e_resolve (term,cl) - | Give_exact (c) -> e_give_exact_constr c + | Give_exact (c) -> e_give_exact c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve (term,cl)) (e_trivial_fail_db db_list local_db) @@ -218,7 +218,7 @@ let e_possible_resolve db_list local_db gl = (fst (head_constr_bound gl)) gl) with Bound | Not_found -> [] -let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id)) +let assumption_tac_list id = apply_tac_list (e_give_exact (mkVar id)) let find_first_goal gls = try first_goal gls with UserError _ -> assert false @@ -266,7 +266,7 @@ module MySearchProblem = struct let l = filter_tactics s.tacres (List.map - (fun id -> (e_give_exact_constr (mkVar id), + (fun id -> (e_give_exact (mkVar id), (str "Exact" ++ spc()++ pr_id id))) (pf_ids_of_hyps g)) in -- cgit v1.2.3