diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-09 15:32:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-09 15:32:28 +0000 |
| commit | 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 (patch) | |
| tree | dc2517398ee4242e9656c7420a5eb5a3c101d82a /plugins | |
| parent | 2a596b2f6df4d884aaec99a519044036a4a81596 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/interface/blast.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |