diff options
author | 2014-06-27 12:45:11 +0200 | |
---|---|---|
committer | 2014-06-27 12:45:11 +0200 | |
commit | 4db867c45dafc7ed7b524a8d089cd57b7944feca (patch) | |
tree | 8d0979ff8570308a56b8db43ec56637ea151e1f6 | |
parent | f25ebf0a2d163df5191cf20650c82955b17972f7 (diff) |
Add an init_setoid check in rewrite to avoid trying to get undefined references.
Fixes the behavior of reflexivity/symmetry etc... when Setoid is not loaded.
-rw-r--r-- | tactics/rewrite.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 06d0a04cc..7b8b0cc55 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1967,7 +1967,8 @@ let setoid_proof ty fn fallback = let rel, args = decompose_app_rel env sigma concl in let evm = sigma in let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in - fn env sigma car rel + (try init_setoid () with _ -> raise Not_found); + fn env sigma car rel with e -> Proofview.tclZERO e end begin function |