aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-03-09 16:43:49 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-03-09 16:43:49 +0100
commitc633bb322acf0bb626eafe6158287d1ddc11af26 (patch)
treedb842a43a788e0a1e24fa27b63e7d9852b3c1666 /tactics/rewrite.ml
parentccd7c003ae56a4f7ad600cfc9532651010fb6bf2 (diff)
Redo fix init_setoid -> init_relation_classes
It got lost during a merge with the 8.5 branch.
Diffstat (limited to 'tactics/rewrite.ml')
-rw-r--r--tactics/rewrite.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1be78c2ad..67d21886b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -2086,7 +2086,7 @@ let setoid_proof ty fn fallback =
let open Context.Rel.Declaration in
let (sigma, t) = Typing.type_of env sigma rel in
let car = get_type (List.hd (fst (Reduction.dest_prod env t))) in
- (try init_setoid () with _ -> raise Not_found);
+ (try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
with e -> Proofview.tclZERO e
end