From 2338a1f27dfb6cb907e1955a7ed3e5316f1df6a0 Mon Sep 17 00:00:00 2001
From: ptorrx <ptorrx@gmail.com>
Date: Fri, 4 Aug 2023 18:36:12 +0200
Subject: [PATCH] adding examples in cmon_enriched_cat.v

---
 HB/instance.elpi  | 2 +-
 HB/structure.elpi | 7 ++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/HB/instance.elpi b/HB/instance.elpi
index 089ac33c..73b453cb 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -783,7 +783,7 @@ redirect-instances RealName Factory TheType TheFactory Body TyWP SectionName Cla
   coq.say "NOW RUNNING****************************** REDIN " 
   coq.say "REDIN!!!!!!! TheTypeKey = " TheTypeKey, 
 
-  if (RealName = "hom_isMon__ELIM")  % meant to rule out generated instances 
+  if (rex.match ".*__ELIM" RealName)  % meant to rule out generated instances 
       (private.dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL)
    (if (TheTypeKey = global TheTypeKeyGR)
     (std.do! [
diff --git a/HB/structure.elpi b/HB/structure.elpi
index e70915d9..4b18fbfb 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -798,11 +798,12 @@ reexport-wrapper-as-instance M :- std.do! [
      coq.env.typeof (const C) Ty,
      coq.count-prods Ty N0,
      coq.term->arity Ty N0 Arity,
-     coq.term->string (global M) Str1,
+%     coq.term->string (global M) Str1,
 %    need to get a valid idenfier out of a term, no @ or .    
 %     std.string.concat "__" [Str1, "ELIM"] Str2, 
-     std.string.concat "__" ["hom_isMon", "ELIM"] Str2, 
-     instance.declare-const Str2 B Arity _
+     Str0 is "Op_isMx" ^ "__" ^ {std.any->string {new_int}},
+     std.string.concat "__" [Str0, "ELIM"] Str, 
+     instance.declare-const Str B Arity _
  ]. 
 
 }}