wip

math-comp · Dec 4, 2023 · faa0803 · faa0803
1 parent 2dbe485
commit faa0803
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/structures.v b/structures.v
@@ -677,8 +677,10 @@ actions-compat ModuleName :-
     end-module _,
   end-module O,
   export-module O,
-  coq.env.current-library File,
-  coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" O)).
+  % is this a bug?
+  % coq.env.current-library File,
+  % coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" O)).
+  true.
 
 main [const-decl N _ _] :- !, with-attributes (actions N).
 

diff --git a/tests/exports.v b/tests/exports.v
@@ -22,6 +22,7 @@ HB.mixin Record Ring_of_TYPE A := {
   mulrDl : left_distributive mul add;
   mulrDr : right_distributive mul add;
 }.
+#[mathcomp]
 HB.structure Definition Ring := { A of Ring_of_TYPE A }.
 
 (* Notations *)