Skip to content

Commit 0a4f725

Browse files
oskgooskgo
committed
fix warnings
1 parent 4a5529b commit 0a4f725

39 files changed

Lines changed: 170 additions & 208 deletions

‎src/ecCoreFol.ml‎

Lines changed: 6 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -274,9 +274,6 @@ let f_eqs fs1 fs2 =
274274
let f_hoareS_r hs = mk_form (FhoareS hs) tbool
275275
let f_hoareF_r hf = mk_form (FhoareF hf) tbool
276276

277-
let f_hoareS_old hs_m hs_pr hs_s hs_po =
278-
f_hoareS_r { hs_m; hs_pr; hs_s; hs_po; }
279-
280277
let f_hoareS hs_mt hs_pr hs_s hs_po =
281278
assert (hs_pr.m = hs_po.m);
282279
f_hoareS_r { hs_m=(hs_pr.m, hs_mt); hs_pr=hs_pr.inv; hs_s;
@@ -286,16 +283,10 @@ let f_hoareF pr hf_f po =
286283
assert (pr.m = po.m);
287284
f_hoareF_r { hf_m=pr.m; hf_pr=pr.inv; hf_f; hf_po=po.inv; } [@alert "-priv_pl"]
288285

289-
let f_hoareF_old hf_pr hf_f hf_po =
290-
f_hoareF_r { hf_m=mhr; hf_pr; hf_f; hf_po; }
291-
292286
(* -------------------------------------------------------------------- *)
293287
let f_eHoareS_r hs = mk_form (FeHoareS hs) tbool
294288
let f_eHoareF_r hf = mk_form (FeHoareF hf) tbool
295289

296-
let f_eHoareS_old ehs_m ehs_pr ehs_s ehs_po =
297-
f_eHoareS_r { ehs_m; ehs_pr; ehs_s; ehs_po; }
298-
299290
let f_eHoareS ehs_mt ehs_pr ehs_s ehs_po =
300291
assert (ehs_pr.m = ehs_po.m);
301292
f_eHoareS_r { ehs_m=(ehs_pr.m, ehs_mt); ehs_pr=ehs_pr.inv; ehs_s;
@@ -506,9 +497,9 @@ let f_map gt g fp =
506497
f_proj f' i ty'
507498

508499
| FhoareF hf ->
509-
let pr' = g hf.hf_pr in
510-
let po' = g hf.hf_po in
511-
f_hoareF_r { hf with hf_pr = pr'; hf_po = po'; }
500+
let pr' = map_ss_inv1 g (hf_pr hf) in
501+
let po' = map_ss_inv1 g (hf_po hf) in
502+
f_hoareF pr' hf.hf_f po'
512503

513504
| FhoareS hs ->
514505
let pr' = g hs.hs_pr in
@@ -574,7 +565,7 @@ let f_iter g f =
574565
| Ftuple es -> List.iter g es
575566
| Fproj (e, _) -> g e
576567

577-
| FhoareF hf -> g hf.hf_pr; g hf.hf_po
568+
| FhoareF hf -> g (hf_pr hf).inv; g (hf_po hf).inv
578569
| FhoareS hs -> g hs.hs_pr; g hs.hs_po
579570
| FeHoareF hf -> g hf.ehf_pr; g hf.ehf_po
580571
| FeHoareS hs -> g hs.ehs_pr; g hs.ehs_po
@@ -603,7 +594,7 @@ let form_exists g f =
603594
| Ftuple es -> List.exists g es
604595
| Fproj (e, _) -> g e
605596

606-
| FhoareF hf -> g hf.hf_pr || g hf.hf_po
597+
| FhoareF hf -> g (hf_pr hf).inv || g (hf_po hf).inv
607598
| FhoareS hs -> g hs.hs_pr || g hs.hs_po
608599
| FeHoareF hf -> g hf.ehf_pr || g hf.ehf_po
609600
| FeHoareS hs -> g hs.ehs_pr || g hs.ehs_po
@@ -631,7 +622,7 @@ let form_forall g f =
631622
| Ftuple es -> List.for_all g es
632623
| Fproj (e, _) -> g e
633624

634-
| FhoareF hf -> g hf.hf_pr && g hf.hf_po
625+
| FhoareF hf -> g (hf_pr hf).inv && g (hf_po hf).inv
635626
| FhoareS hs -> g hs.hs_pr && g hs.hs_po
636627
| FbdHoareF bhf -> g bhf.bhf_pr && g bhf.bhf_po
637628
| FbdHoareS bhs -> g bhs.bhs_pr && g bhs.bhs_po

‎src/ecCoreFol.mli‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -114,13 +114,10 @@ val f_lambda : bindings -> form -> form
114114
val f_forall_mems : (EcIdent.t * memtype) list -> form -> form
115115

116116
val f_hoareF : ss_inv -> xpath -> ss_inv -> form
117-
val f_hoareF_old : form -> xpath -> form -> form
118117
val f_hoareS : memtype -> ss_inv -> stmt -> ss_inv -> form
119-
val f_hoareS_old : memenv -> form -> stmt -> form -> form
120118

121119
val f_eHoareF_old : form -> xpath -> form -> form
122120
val f_eHoareF : ss_inv -> xpath -> ss_inv -> form
123-
val f_eHoareS_old : memenv -> form -> EcCoreModules.stmt -> form -> form
124121
val f_eHoareS : memtype -> ss_inv -> EcCoreModules.stmt -> ss_inv -> form
125122

126123
(* soft-constructors - eager *)

‎src/ecCoreSubst.ml‎

Lines changed: 28 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -453,66 +453,65 @@ module Fsubst = struct
453453
| FhoareF hf ->
454454
let hf_f = x_subst s hf.hf_f in
455455
let (s, m) = add_m_binding s hf.hf_m in
456-
let hf_pr = f_subst ~tx s hf.hf_pr [@alert "-priv_pl"] in
457-
let hf_po = f_subst ~tx s hf.hf_po [@alert "-priv_pl"] in
456+
let hf_pr = f_subst ~tx s (hf_pr hf).inv in
457+
let hf_po = f_subst ~tx s (hf_po hf).inv in
458458
f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po}
459459

460460
| FhoareS hs ->
461461
let hs_s = s_subst s hs.hs_s in
462-
let s, hs_m = add_me_binding s hs.hs_m in
463-
let m = fst hs_m in
464-
let hs_pr = f_subst ~tx s hs.hs_pr in
465-
let hs_po = f_subst ~tx s hs.hs_po in
466-
f_hoareS (snd hs_m) {m;inv=hs_pr} hs_s {m;inv=hs_po}
462+
let s, (m, mt) = add_me_binding s hs.hs_m in
463+
let hs_pr = f_subst ~tx s (hs_pr hs).inv in
464+
let hs_po = f_subst ~tx s (hs_po hs).inv in
465+
f_hoareS mt {m;inv=hs_pr} hs_s {m;inv=hs_po}
467466

468467
| FeHoareF hf ->
469468
let hf_f = x_subst s hf.ehf_f in
470469
let (s, m) = add_m_binding s hf.ehf_m in
471-
let hf_pr = f_subst ~tx s hf.ehf_pr in
472-
let hf_po = f_subst ~tx s hf.ehf_po in
473-
f_eHoareF_old hf_pr hf_f hf_po
470+
let hf_pr = f_subst ~tx s (ehf_pr hf).inv in
471+
let hf_po = f_subst ~tx s (ehf_po hf).inv in
472+
f_eHoareF {m;inv=hf_pr} hf_f {m;inv=hf_po}
474473

475474
| FeHoareS hs ->
476475
let hs_s = s_subst s hs.ehs_s in
477-
let s, hs_m = add_me_binding s hs.ehs_m in
478-
let hs_pr = f_subst ~tx s hs.ehs_pr in
479-
let hs_po = f_subst ~tx s hs.ehs_po in
480-
f_eHoareS_old hs_m hs_pr hs_s hs_po
476+
let s, (m, mt) = add_me_binding s hs.ehs_m in
477+
let hs_pr = f_subst ~tx s (ehs_pr hs).inv in
478+
let hs_po = f_subst ~tx s (ehs_po hs).inv in
479+
f_eHoareS mt {m;inv=hs_pr} hs_s {m;inv=hs_po}
481480

482481
| FbdHoareF hf ->
483482
let hf_f = x_subst s hf.bhf_f in
484483
let (s, m) = add_m_binding s hf.bhf_m in
485-
let hf_pr = f_subst ~tx s hf.bhf_pr in
486-
let hf_po = f_subst ~tx s hf.bhf_po in
487-
let hf_bd = f_subst ~tx s hf.bhf_bd in
484+
let hf_pr = f_subst ~tx s (bhf_pr hf).inv in
485+
let hf_po = f_subst ~tx s (bhf_po hf).inv in
486+
let hf_bd = f_subst ~tx s (bhf_bd hf).inv in
488487
f_bdHoareF {m;inv=hf_pr} hf_f {m;inv=hf_po} hf.bhf_cmp {m;inv=hf_bd}
489488

490489
| FbdHoareS hs ->
491490
let hs_s = s_subst s hs.bhs_s in
492491
let s, hs_m = add_me_binding s hs.bhs_m in
493492
let m = fst hs_m in
494-
let hs_pr = f_subst ~tx s hs.bhs_pr in
495-
let hs_po = f_subst ~tx s hs.bhs_po in
496-
let hs_bd = f_subst ~tx s hs.bhs_bd in
493+
let hs_pr = f_subst ~tx s (bhs_pr hs).inv in
494+
let hs_po = f_subst ~tx s (bhs_po hs).inv in
495+
let hs_bd = f_subst ~tx s (bhs_bd hs).inv in
497496
f_bdHoareS (snd hs_m) {m;inv=hs_pr} hs_s {m;inv=hs_po} hs.bhs_cmp {m;inv=hs_bd}
498497

499498
| FequivF ef ->
500499
let ef_fl = x_subst s ef.ef_fl in
501500
let ef_fr = x_subst s ef.ef_fr in
502501
let (s, ml) = add_m_binding s ef.ef_ml in
503502
let (s, mr) = add_m_binding s ef.ef_mr in
504-
let ef_pr = f_subst ~tx s ef.ef_pr in
505-
let ef_po = f_subst ~tx s ef.ef_po in
503+
let ef_pr = f_subst ~tx s (ef_pr ef).inv in
504+
let ef_po = f_subst ~tx s (ef_po ef).inv in
506505
f_equivF {ml;mr;inv=ef_pr} ef_fl ef_fr {ml;mr;inv=ef_po}
507506

508507
| FequivS es ->
509508
let es_sl = s_subst s es.es_sl in
510509
let es_sr = s_subst s es.es_sr in
511-
let s, es_ml = add_me_binding s es.es_ml in
512-
let s, es_mr = add_me_binding s es.es_mr in
513-
let es_pr = f_subst ~tx s es.es_pr in
514-
let es_po = f_subst ~tx s es.es_po in
515-
f_equivS_old es_ml es_mr es_pr es_sl es_sr es_po
510+
let s, (ml, mlt) = add_me_binding s es.es_ml in
511+
let s, (mr, mrt) = add_me_binding s es.es_mr in
512+
let es_pr = f_subst ~tx s (es_pr es).inv in
513+
let es_po = f_subst ~tx s (es_po es).inv in
514+
f_equivS mlt mrt {ml;mr;inv=es_pr} es_sl es_sr {ml;mr;inv=es_po}
516515

517516
| FeagerF eg ->
518517
let eg_fl = x_subst s eg.eg_fl in
@@ -521,8 +520,8 @@ module Fsubst = struct
521520
let eg_sr = s_subst s eg.eg_sr in
522521
let (s, ml) = add_m_binding s eg.eg_ml in
523522
let (s, mr) = add_m_binding s eg.eg_mr in
524-
let eg_pr = f_subst ~tx s eg.eg_pr in
525-
let eg_po = f_subst ~tx s eg.eg_po in
523+
let eg_pr = f_subst ~tx s (eg_pr eg).inv in
524+
let eg_po = f_subst ~tx s (eg_po eg).inv in
526525
f_eagerF {ml;mr;inv=eg_pr} eg_sl eg_fl eg_fr eg_sr {ml;mr;inv=eg_po}
527526

528527
| Fpr pr ->

‎src/ecFol.mli‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
(* -------------------------------------------------------------------- *)
22
open EcBigInt
33
open EcPath
4-
open EcTypes
5-
open EcMemory
64
open EcAst
75

86
(* -------------------------------------------------------------------- *)

‎src/ecLowPhlGoal.ml‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -210,7 +210,7 @@ let tc1_get_stmt side tc =
210210
let hl_set_stmt (side : side option) (f : form) (s : stmt) =
211211
match side, f.f_node with
212212
| None , FhoareS hs -> f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs)
213-
| None , FeHoareS hs -> f_eHoareS_old hs.ehs_m hs.ehs_pr s hs.ehs_po
213+
| None , FeHoareS hs -> f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s (ehs_po hs)
214214
| None , FbdHoareS hs -> f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
215215
| Some `Left , FequivS es -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) s es.es_sr (es_po es)
216216
| Some `Right, FequivS es -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl s (es_po es)
@@ -264,10 +264,10 @@ let set_pre ~pre f =
264264
f_hoareS (snd hs.hs_m) pre hs.hs_s (hs_po hs)
265265
| FeHoareF hf, Inv_ss pre ->
266266
let pre = ss_inv_rebind pre hf.ehf_m in
267-
f_eHoareF_old pre.inv hf.ehf_f hf.ehf_po
267+
f_eHoareF pre hf.ehf_f (ehf_po hf)
268268
| FeHoareS hs, Inv_ss pre ->
269269
let pre = ss_inv_rebind pre (fst hs.ehs_m) in
270-
f_eHoareS_old hs.ehs_m pre.inv hs.ehs_s hs.ehs_po
270+
f_eHoareS (snd hs.ehs_m) pre hs.ehs_s (ehs_po hs)
271271
| FbdHoareF hf, Inv_ss pre ->
272272
let pre = ss_inv_rebind pre hf.bhf_m in
273273
f_bdHoareF pre hf.bhf_f (bhf_po hf) hf.bhf_cmp (bhf_bd hf)
@@ -279,7 +279,7 @@ let set_pre ~pre f =
279279
f_equivF pre ef.ef_fl ef.ef_fr (ef_po ef)
280280
| FequivS es, Inv_ts pre ->
281281
let pre = ts_inv_rebind pre (fst es.es_ml) (fst es.es_mr) in
282-
f_equivS_old es.es_ml es.es_mr pre.inv es.es_sl es.es_sr es.es_po
282+
f_equivS (snd es.es_ml) (snd es.es_mr) pre es.es_sl es.es_sr (es_po es)
283283
| _ -> assert false
284284

285285
(* -------------------------------------------------------------------- *)
@@ -690,11 +690,11 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
690690
match side with
691691
| `Left -> (es.es_ml, es.es_sl)
692692
| `Right -> (es.es_mr, es.es_sr) in
693-
let me, stmt, cs = tx (pf, hyps) cpos (pre, post) (me, stmt) in
693+
let (_, mt), stmt, cs = tx (pf, hyps) cpos (pre, post) (me, stmt) in
694694
let concl =
695695
match side with
696-
| `Left -> f_equivS_old me es.es_mr es.es_pr stmt es.es_sr es.es_po
697-
| `Right -> f_equivS_old es.es_ml me es.es_pr es.es_sl stmt es.es_po
696+
| `Left -> f_equivS mt (snd es.es_mr) (es_pr es) stmt es.es_sr (es_po es)
697+
| `Right -> f_equivS (snd es.es_ml) mt (es_pr es) es.es_sl stmt (es_po es)
698698
in
699699

700700
FApi.xmutate1 tc (tr (Some side)) (cs @ [concl])

‎src/ecMatching.ml‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -692,7 +692,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
692692
assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs));
693693
let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in
694694
List.iter2 (doit env (subst, mxs))
695-
[hf1.hf_pr; hf1.hf_po] [hf2.hf_pr; hf2.hf_po]
695+
[(hf_pr hf1).inv; (hf_po hf1).inv] [(hf_pr hf2).inv; (hf_po hf2).inv]
696696
end
697697

698698
| FbdHoareF hf1, FbdHoareF hf2 -> begin
@@ -994,12 +994,12 @@ module FPosition = struct
994994
doit pos (`WithSubCtxt [(ctxt, pr.pr_args); (subctxt, pr.pr_event)])
995995

996996
| FhoareF hs ->
997-
doit pos (`WithCtxt (Sid.add EcFol.mhr ctxt, [hs.hf_pr; hs.hf_po]))
997+
doit pos (`WithCtxt (Sid.add hs.hf_m ctxt, [(hf_pr hs).inv; (hf_po hs).inv]))
998998

999999
(* TODO: A: From what I undertand, there is an error there:
10001000
it should be (subctxt, hs.bhf_bd) *)
10011001
| FbdHoareF hs ->
1002-
let subctxt = Sid.add EcFol.mhr ctxt in
1002+
let subctxt = Sid.add hs.bhf_m ctxt in
10031003
doit pos (`WithSubCtxt ([(subctxt, hs.bhf_pr);
10041004
(subctxt, hs.bhf_po);
10051005
( ctxt, hs.bhf_bd)]))
@@ -1142,15 +1142,16 @@ module FPosition = struct
11421142
f_pr pr.pr_mem pr.pr_fun args' event'
11431143

11441144
| FhoareF hf ->
1145-
let (hf_pr, hf_po) = as_seq2 (doit p [hf.hf_pr; hf.hf_po]) in
1145+
let (hf_pr, hf_po) = as_seq2 (doit p [(hf_pr hf).inv; (hf_po hf).inv]) in
11461146
let m = hf.hf_m in
11471147
f_hoareF {m;inv=hf_pr} hf.hf_f {m;inv=hf_po}
11481148

11491149
| FeHoareF hf ->
11501150
let (ehf_pr, ehf_po) =
11511151
as_seq2 (doit p [hf.ehf_pr; hf.ehf_po;])
11521152
in
1153-
f_eHoareF_old ehf_pr hf.ehf_f ehf_po
1153+
let m = hf.ehf_m in
1154+
f_eHoareF {m;inv=ehf_pr} hf.ehf_f {m;inv=ehf_po}
11541155

11551156
| FbdHoareF hf ->
11561157
let sub = doit p [hf.bhf_pr; hf.bhf_po; hf.bhf_bd] in

‎src/ecPV.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -329,32 +329,32 @@ module PV = struct
329329
aux env fv e
330330

331331
| FhoareF hf ->
332-
in_mem_scope env fv [mhr] [hf.hf_pr; hf.hf_po]
332+
in_mem_scope env fv [hf.hf_m] [(hf_pr hf).inv; (hf_po hf).inv]
333333

334334
| FhoareS hs ->
335335
in_mem_scope env fv [fst hs.hs_m] [hs.hs_pr; hs.hs_po]
336336

337337
| FeHoareF hf ->
338-
in_mem_scope env fv [mhr] [hf.ehf_pr; hf.ehf_po]
338+
in_mem_scope env fv [hf.ehf_m] [hf.ehf_pr; hf.ehf_po]
339339

340340
| FeHoareS hs ->
341341
in_mem_scope env fv [fst hs.ehs_m] [hs.ehs_pr; hs.ehs_po]
342342

343343
| FbdHoareF bhf ->
344-
in_mem_scope env fv [mhr] [bhf.bhf_pr; bhf.bhf_po; bhf.bhf_bd]
344+
in_mem_scope env fv [bhf.bhf_m] [bhf.bhf_pr; bhf.bhf_po; bhf.bhf_bd]
345345

346346
| FbdHoareS bhs ->
347347
in_mem_scope env fv
348348
[fst bhs.bhs_m] [bhs.bhs_pr; bhs.bhs_po; bhs.bhs_bd]
349349

350350
| FequivF ef ->
351-
in_mem_scope env fv [mleft; mright] [ef.ef_pr; ef.ef_po]
351+
in_mem_scope env fv [ef.ef_ml; ef.ef_mr] [ef.ef_pr; ef.ef_po]
352352

353353
| FequivS es ->
354354
in_mem_scope env fv [fst es.es_ml; fst es.es_mr] [es.es_pr; es.es_po]
355355

356356
| FeagerF eg ->
357-
in_mem_scope env fv [mhr] [eg.eg_pr; eg.eg_po]
357+
in_mem_scope env fv [eg.eg_ml; eg.eg_mr] [eg.eg_pr; eg.eg_po]
358358

359359
| Fpr pr ->
360360
let fv = aux env fv pr.pr_args in

‎src/ecPV.mli‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,7 @@
11
(* -------------------------------------------------------------------- *)
22
open EcMaps
33
open EcPath
4-
open EcTypes
5-
open EcModules
6-
open EcMemory
74
open EcEnv
8-
open EcFol
95
open EcAst
106

117
(* -------------------------------------------------------------------- *)

‎src/ecPrinting.ml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1938,13 +1938,13 @@ and pp_form_core_r
19381938
Format.fprintf fmt "hoare[@[<hov 2>@ %a {%a} :@ @[%a ==>@ %a@]@]]"
19391939
(pp_funname ppe) hf.hf_f
19401940
(pp_mem ppe) hf.hf_m
1941-
(pp_form ppepr) hf.hf_pr
1942-
(pp_form ppepo) hf.hf_po
1941+
(pp_form ppepr) (hf_pr hf).inv
1942+
(pp_form ppepo) (hf_po hf).inv
19431943
else
19441944
Format.fprintf fmt "hoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]]"
19451945
(pp_funname ppe) hf.hf_f
1946-
(pp_form ppepr) hf.hf_pr
1947-
(pp_form ppepo) hf.hf_po
1946+
(pp_form ppepr) (hf_pr hf).inv
1947+
(pp_form ppepo) (hf_po hf).inv
19481948

19491949
| FhoareS hs ->
19501950
let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
@@ -2986,12 +2986,12 @@ let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf =
29862986
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
29872987
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
29882988

2989-
Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) hf.hf_pr;
2989+
Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (hf_pr hf).inv;
29902990
if debug_mode then
29912991
Format.fprintf fmt " %a {%a}@\n%!" (pp_funname ppe) hf.hf_f (pp_mem ppe) hf.hf_m
29922992
else
29932993
Format.fprintf fmt " %a@\n%!" (pp_funname ppe) hf.hf_f;
2994-
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) hf.hf_po
2994+
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (hf_po hf).inv
29952995

29962996
(* -------------------------------------------------------------------- *)
29972997

‎src/ecProofTyping.mli‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,9 @@
11
(* -------------------------------------------------------------------- *)
22
open EcParsetree
33
open EcIdent
4-
open EcTypes
5-
open EcFol
64
open EcDecl
7-
open EcModules
85
open EcEnv
96
open EcCoreGoal
10-
open EcMemory
117
open EcMatching.Position
128
open EcAst
139

0 commit comments

Comments
 (0)