diff options
| author | herbelin | 2010-09-19 10:18:01 +0000 |
|---|---|---|
| committer | herbelin | 2010-09-19 10:18:01 +0000 |
| commit | 99aa9904cb19255a154937a0cca39fbc536ffe97 (patch) | |
| tree | 04ef97db1dd47396a1d936224bc0b5cf697af88f | |
| 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
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 6 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 16 |
2 files changed, 12 insertions, 10 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index fa0e76841a..e625fe3b4e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -455,9 +455,9 @@ let setoid_of_relation env a r = try lapp coq_mk_Setoid [|a ; r ; - Rewrite.get_reflexive_proof env evm a r ; - Rewrite.get_symmetric_proof env evm a r ; - Rewrite.get_transitive_proof env evm a r |] + fst (Rewrite.get_reflexive_proof env evm a r) ; + fst (Rewrite.get_symmetric_proof env evm a r) ; + fst (Rewrite.get_transitive_proof env evm a r) |] with Not_found -> error "cannot find setoid relation" diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 4524cf0dae..921137842c 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 = |