diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 6 |
1 files changed, 3 insertions, 3 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" |