fix #211 where defining a lossless distribution without requiring Distr makes rnd panic

Co-authored-by: Copilot <copilot@github.com>

Author: 2 people

src/ecScope.ml

@@ -1431,8 +1431,8 @@ module Op = struct
     let add_distr_tag
         (pred : path) (bases : string list) (tag : string) (suffix : string) scope
     =
-      if not (EcAlgTactic.is_module_loaded (env scope)) then
-        hierror "for tag %s, load Distr first" tag;
+      if EcEnv.Op.by_path_opt pred (env scope) = None then
+         hierror "for tag %s, load Distr first" tag;
 
       let oppath   = EcPath.pqname (path scope) (unloc op.po_name) in
       let nparams  = List.map EcIdent.fresh tyop.op_tparams in

tests/rnd_ll.ec

@@ -0,0 +1,19 @@
+require import AllCore.
+
+fail op[lossless] dC : bool distr.
+
+require import Distr.
+
+op[lossless] dC : bool distr.
+
+module M = { 
+  proc p1() = {
+    var e1;
+    e1 <$ dC;
+  }
+}.
+
+equiv foo : M.p1 ~ M.p1 : true ==> true.
+proc. 
+rnd.
+abort.

theories/crypto/DigitalSignatures.eca

@@ -12,7 +12,7 @@
 
 (* --- Require/Import Theories --- *)
 (* -- Built-in (i.e, standard library) -- *)
-require import AllCore List.
+require import AllCore List Distr.