diff options
| author | msozeau | 2008-09-09 08:55:34 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-09 08:55:34 +0000 |
| commit | 85972057e714da016b9299f47b833aec31220403 (patch) | |
| tree | 9e28b119cd0457b2990cf549ab64e857bd4e3038 /tactics | |
| parent | bd7f800d5fc48dcb7bfae475e796f6e18901fbcb (diff) | |
Fix a bug reintroduced in [setoid_reflexivity] etc...
Go back to refine_hyp instead of specialize, because only the former
handles open terms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11391 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e803e8dcbc..22e95ef5d8 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1734,14 +1734,20 @@ let relation_of_constr env c = let setoid_proof gl ty fn fallback = let env = pf_env gl in - let rel, args = relation_of_constr env (pf_concl gl) in - let evm, car = project gl, pf_type_of gl args.(0) in - try fn env evm car rel gl - with Not_found -> + try + let rel, args = relation_of_constr env (pf_concl gl) in + let evm, car = project gl, pf_type_of gl args.(0) in + fn env evm car rel gl + with e -> match fallback gl with | Some tac -> tac gl - | None -> not_declared env ty rel gl - + | None -> + match e with + | Not_found -> + let rel, args = relation_of_constr env (pf_concl gl) in + not_declared env ty rel gl + | _ -> raise e + let setoid_reflexivity gl = setoid_proof gl "reflexive" (fun env evm car rel -> apply (get_reflexive_proof env evm car rel)) |