File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -439,17 +439,7 @@ let ov_equal vd1 vd2 =
439439 EcUtils. opt_equal (= ) vd1.ov_name vd2.ov_name &&
440440 ty_equal vd1.ov_type vd2.ov_type
441441
442- let v_hash v =
443- Why3.Hashcons. combine
444- (Hashtbl. hash v.v_name)
445- (ty_hash v.v_type)
446-
447- let v_equal vd1 vd2 =
448- vd1.v_name = vd2.v_name &&
449- ty_equal vd1.v_type vd2.v_type
450-
451442(* -------------------------------------------------------------------- *)
452-
453443let mr_xpaths (mr : mod_restr ) : mr_xpaths =
454444 { ur_pos = omap fst mr.ur_pos;
455445 ur_neg = fst mr.ur_neg; }
@@ -624,15 +614,6 @@ let b_hash (bs : bindings) =
624614 in
625615 Why3.Hashcons. combine_list b1_hash 0 bs
626616
627- (* -------------------------------------------------------------------- *)
628- let i_equal = ((== ) : instr -> instr -> bool )
629- let i_hash = fun i -> i.i_tag
630- let i_fv i = i.i_fv
631-
632- let s_equal = ((== ) : stmt -> stmt -> bool )
633- let s_hash = fun s -> s.s_tag
634- let s_fv = fun s -> s.s_fv
635-
636617(* -------------------------------------------------------------------- *)
637618let hf_equal hf1 hf2 =
638619 f_equal hf1.hf_pr hf2.hf_pr
Original file line number Diff line number Diff line change @@ -344,9 +344,6 @@ val hcmp_hash : hoarecmp hash
344344val ov_equal : ovariable equality
345345val ov_hash : ovariable hash
346346
347- val v_equal : variable equality
348- val v_hash : variable hash
349-
350347(* -------------------------------------------------------------------- *)
351348val ur_equal : 'a equality -> 'a use_restr equality
352349val ur_hash : ('a -> 'b list ) -> 'b hash -> 'a use_restr hash
@@ -389,19 +386,9 @@ val gty_hash : gty hash
389386val gty_fv : gty fv
390387
391388(* -------------------------------------------------------------------- *)
392-
393389val b_equal : bindings equality
394390val b_hash : bindings hash
395391
396- (* -------------------------------------------------------------------- *)
397- val i_equal : instr equality
398- val i_hash : instr hash
399- val i_fv : instr fv
400-
401- val s_equal : stmt equality
402- val s_hash : stmt hash
403- val s_fv : stmt fv
404-
405392(* -------------------------------------------------------------------- *)
406393val hf_equal : sHoareF equality
407394val hf_hash : sHoareF hash
You can’t perform that action at this time.
0 commit comments