File tree Expand file tree Collapse file tree 1 file changed +4
-2
lines changed Expand file tree Collapse file tree 1 file changed +4
-2
lines changed Original file line number Diff line number Diff line change @@ -589,7 +589,9 @@ let wp_equiv_rnd_r bij tc =
589589let t_equiv_rnd_r side pos bij_info tc =
590590 match side, pos, bij_info with
591591 | Some side , None , (None, None) ->
592- wp_equiv_disj_rnd_r side tc
592+ wp_equiv_disj_rnd_r side tc
593+ | Some side , None , _ ->
594+ tc_error !! tc " one-sided rnd takes no arguments"
593595 | None , _ , _ -> begin
594596 let pos =
595597 match pos with
@@ -617,7 +619,7 @@ let t_equiv_rnd_r side pos bij_info tc =
617619 end
618620
619621 | _ ->
620- tc_error !! tc " invalid argument "
622+ tc_error !! tc " two-sided rnd requires a bijection "
621623
622624(* -------------------------------------------------------------------- *)
623625let wp_equiv_disj_rnd = FApi. t_low1 " wp-equiv-disj-rnd" wp_equiv_disj_rnd_r
You can’t perform that action at this time.
0 commit comments