File tree Expand file tree Collapse file tree 2 files changed +0
-32
lines changed Expand file tree Collapse file tree 2 files changed +0
-32
lines changed Original file line number Diff line number Diff line change @@ -439,17 +439,7 @@ let ov_equal vd1 vd2 =
439
439
EcUtils. opt_equal (= ) vd1.ov_name vd2.ov_name &&
440
440
ty_equal vd1.ov_type vd2.ov_type
441
441
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
-
451
442
(* -------------------------------------------------------------------- *)
452
-
453
443
let mr_xpaths (mr : mod_restr ) : mr_xpaths =
454
444
{ ur_pos = omap fst mr.ur_pos;
455
445
ur_neg = fst mr.ur_neg; }
@@ -624,15 +614,6 @@ let b_hash (bs : bindings) =
624
614
in
625
615
Why3.Hashcons. combine_list b1_hash 0 bs
626
616
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
-
636
617
(* -------------------------------------------------------------------- *)
637
618
let hf_equal hf1 hf2 =
638
619
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
344
344
val ov_equal : ovariable equality
345
345
val ov_hash : ovariable hash
346
346
347
- val v_equal : variable equality
348
- val v_hash : variable hash
349
-
350
347
(* -------------------------------------------------------------------- *)
351
348
val ur_equal : 'a equality -> 'a use_restr equality
352
349
val ur_hash : ('a -> 'b list ) -> 'b hash -> 'a use_restr hash
@@ -389,19 +386,9 @@ val gty_hash : gty hash
389
386
val gty_fv : gty fv
390
387
391
388
(* -------------------------------------------------------------------- *)
392
-
393
389
val b_equal : bindings equality
394
390
val b_hash : bindings hash
395
391
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
-
405
392
(* -------------------------------------------------------------------- *)
406
393
val hf_equal : sHoareF equality
407
394
val hf_hash : sHoareF hash
You can’t perform that action at this time.
0 commit comments