eqbOK: fresh names

Author: eponier

apps/derive/elpi/eqbOK.elpi

@@ -36,7 +36,7 @@ main (indt I) Prefix [CL] :- std.do! [
   add-reflect FI (global (const Correct)) (global (const Refl)) Breflect,
 
   std.assert-ok! (coq.typecheck Breflect Treflect) "eqbOK generates illtyped term", 
-  Namerf is Prefix ^ "eqb_OK",
+  coq.ensure-fresh-global-id (Prefix ^ "eqb_OK") Namerf,
   coq.env.add-const Namerf Breflect Treflect @opaque! Reflect,
 
   CL = eqbok-for (indt I) Reflect,
@@ -50,7 +50,7 @@ main (const C) Prefix [CL] :- std.do! [
   add-reflect (inductive _ _) (global (const Correct)) (global (const Refl)) Breflect,
 
   std.assert-ok! (coq.typecheck Breflect _) "eqbOK generates illtyped term", 
-  Namerf is Prefix ^ "eqb_OK",
+  coq.ensure-fresh-global-id (Prefix ^ "eqb_OK") Namerf,
   X = global (const C),
   coq.env.add-const Namerf Breflect {{ forall a b : lp:X, Bool.reflect (@eq lp:X a b) (lp:F a b) }} @opaque! Reflect,
   CL = eqbok-for (const C) Reflect,

apps/derive/theories/derive/eqbOK.v

@@ -26,20 +26,15 @@ Elpi Accumulate Db derive.eqbOK.db.
 Elpi Accumulate File eqbOK.
 Elpi Accumulate File eqType.
 Elpi Accumulate lp:{{
- main [str I, str O] :- !, 
-    coq.locate I GR, 
-    Prefix is O ^ "_",
-    derive.eqbOK.main GR Prefix _.
-
   main [str I] :- !, 
     coq.locate I GR,
     coq.gref->id GR Tname,
     Prefix is Tname ^ "_",
     derive.eqbOK.main GR Prefix _.
 
   main _ :- usage.
-   
-  usage :- coq.error "Usage: derive.eqbOK <inductive name/alias> [<prefix>]".
+
+  usage :- coq.error "Usage: derive.eqbOK <inductive name/alias>".
 
 }}.
 Elpi Typecheck.