diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-19 10:18:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-19 10:18:01 +0000 |
| commit | 99aa9904cb19255a154937a0cca39fbc536ffe97 (patch) | |
| tree | 04ef97db1dd47396a1d936224bc0b5cf697af88f /tactics/rewrite.ml4 | |
| parent | acda433289896a8aea287cc9f510e9a874623533 (diff) | |
Patch solving the bug but leaving open design choices
The patch does not address the possible use of evars by get_symmetric_proof in
unify_eqn. Someting has still to be done there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13435 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 4524cf0da..921137842 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -222,7 +222,7 @@ let find_class_proof proof_type proof_method env evars carrier relation = try let goal = mkApp (Lazy.force proof_type, [| carrier ; relation |]) in let evars, c = Typeclasses.resolve_one_typeclass env evars goal in - mkApp (Lazy.force proof_method, [| carrier; relation; c |]) + mkApp (Lazy.force proof_method, [| carrier; relation; c |]), evars with e when Logic.catchable_exception e -> raise Not_found let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env @@ -368,7 +368,7 @@ let unify_eqn env sigma hypinfo t = let res = if l2r then (prf, (car, rel, c1, c2)) else - try (mkApp (get_symmetric_proof env Evd.empty car rel, + try (mkApp (fst (get_symmetric_proof env Evd.empty car rel), [| c1 ; c2 ; prf |]), (car, rel, c2, c1)) with Not_found -> @@ -1626,23 +1626,25 @@ let setoid_proof gl ty fn fallback = not_declared env ty rel gl | _ -> raise e +let apply_with_evars (c,evars) = tclTHEN (Refiner.tclEVARS evars) (apply c) + let setoid_reflexivity gl = setoid_proof gl "reflexive" - (fun env evm car rel -> apply (get_reflexive_proof env evm car rel)) + (fun env evm car rel -> apply_with_evars (get_reflexive_proof env evm car rel)) (reflexivity_red true) let setoid_symmetry gl = setoid_proof gl "symmetric" - (fun env evm car rel -> apply (get_symmetric_proof env evm car rel)) + (fun env evm car rel -> apply_with_evars (get_symmetric_proof env evm car rel)) (symmetry_red true) let setoid_transitivity c gl = setoid_proof gl "transitive" (fun env evm car rel -> - let proof = get_transitive_proof env evm car rel in + let proof,evm = get_transitive_proof env evm car rel in match c with - | None -> eapply proof - | Some c -> apply_with_bindings (proof,Rawterm.ImplicitBindings [ c ])) + | None -> tclTHEN (Refiner.tclEVARS evm) (eapply proof) + | Some c -> tclTHEN (Refiner.tclEVARS evm) (apply_with_bindings (proof,Rawterm.ImplicitBindings [ c ]))) (transitivity_red true c) let setoid_symmetry_in id gl = |