nits

EasyCrypt · Oct 8, 2024 · 8c89fe4 · 8c89fe4
1 parent fc489e6
commit 8c89fe4
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 9 deletions.
diff --git a/src/ecScope.ml b/src/ecScope.ml
@@ -2316,6 +2316,7 @@ end = struct
     name      : symbol;
     types_    : (symbol * path) list;
     operators : (symbol * preoperator) list;
+    proofs    : symbol list;
   }
 
   let doclone (scope : scope) (clone : clone) =
@@ -2343,9 +2344,10 @@ end = struct
           evc_types  = Msym.of_list (List.map do_type clone.types_);
           evc_ops    = Msym.of_list (List.map do_operator clone.operators);
           evc_lemmas = {
-            ev_bynames = Msym.of_list [
-              "ge0_size", (Some (loced (Pby None)), `Alias, false)
-            ];
+            ev_bynames =
+              clone.proofs
+                |> List.map (fun name -> (name, (Some (loced (Pby None)), `Alias, false)))
+                |> Msym.of_list;
             ev_global  = [None, None]; } } in
 
     let npath = EcPath.pqname (EcEnv.root env) clone.name in
@@ -2388,7 +2390,8 @@ end = struct
       ; operators =
           [ ("size"  , `Int bs.size)
           ; ("tolist", `Path to_)
-          ; ("oflist", `Path from_) ] } in
+          ; ("oflist", `Path from_) ]
+      ; proofs    = ["ge0_size"] } in
 
     let proofs, scope = doclone scope preclone in
 

diff --git a/src/phl/ecPhlBDep.ml b/src/phl/ecPhlBDep.ml
@@ -6,7 +6,6 @@ open EcPath
 open EcParsetree
 open EcEnv
 open EcTypes
-open EcModules
 open EcCoreGoal
 open EcAst
 open EcCoreFol
@@ -256,26 +255,26 @@ let t_circ (tc: tcenv1) : tcenv =
 
   let w2bits (env: env) (ty: ty) (arg: form) : form = 
     let tb = match EcEnv.Circ.lookup_bitstring env ty with
-    | Some {to_bits=tb; _} -> tb
+    | Some {to_=tb; _} -> tb
     | _ -> Format.eprintf "No w2bits for type %a@." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty; assert false
     in EcTypesafeFol.f_app_safe env tb [arg]
 
   let bits2w (env: env) (ty: ty) (arg: form) : form = 
     let fb = match EcEnv.Circ.lookup_bitstring env ty with
-    | Some {from_bits=fb; _} -> fb
+    | Some {from_=fb; _} -> fb
     | _ -> Format.eprintf "No bits2w for type %a@." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty; assert false
     in EcTypesafeFol.f_app_safe env fb [arg]
 
   let w2bits_op (env: env) (ty: ty) : form = 
     let tb = match EcEnv.Circ.lookup_bitstring env ty with
-    | Some {to_bits=tb; _} -> tb
+    | Some {to_=tb; _} -> tb
     | _ -> Format.eprintf "No bits2w for type %a@." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty; assert false
     in let tbp, tbo = EcEnv.Op.lookup (EcPath.toqsymbol tb) env in
     f_op tb [] tbo.op_ty 
 
   let bits2w_op (env: env) (ty: ty) : form = 
     let fb = match EcEnv.Circ.lookup_bitstring env ty with
-    | Some {from_bits=fb; _} -> fb
+    | Some {from_=fb; _} -> fb
     | _ -> Format.eprintf "No bits2w for type %a@." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty; assert false
     in let fbp, fbo = EcEnv.Op.lookup (EcPath.toqsymbol fb) env in
     f_op fb [] fbo.op_ty