adding examples in cmon_enriched_cat.v

math-comp · Aug 4, 2023 · 2338a1f · 2338a1f
1 parent f8da435
commit 2338a1f
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git 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
@@ -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 _
  ]. 
 
 }}