We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b5eb295 commit 3ee0c81Copy full SHA for 3ee0c81
1 file changed
src/phl/ecPhlRnd.ml
@@ -589,7 +589,9 @@ let wp_equiv_rnd_r bij tc =
589
let t_equiv_rnd_r side pos bij_info tc =
590
match side, pos, bij_info with
591
| Some side, None, (None, None) ->
592
- wp_equiv_disj_rnd_r side tc
+ wp_equiv_disj_rnd_r side tc
593
+ | Some side, None, _ ->
594
+ tc_error !!tc "one-sided rnd takes no arguments"
595
| None, _, _ -> begin
596
let pos =
597
match pos with
@@ -617,7 +619,7 @@ let t_equiv_rnd_r side pos bij_info tc =
617
619
end
618
620
621
| _ ->
- tc_error !!tc "invalid argument"
622
+ tc_error !!tc "two-sided rnd requires a bijection"
623
624
(* -------------------------------------------------------------------- *)
625
let wp_equiv_disj_rnd = FApi.t_low1 "wp-equiv-disj-rnd" wp_equiv_disj_rnd_r
0 commit comments