From faa08036e399d97a8117e1c1f362bd7554632446 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Dec 2023 17:56:12 +0100 Subject: [PATCH] wip --- structures.v | 6 ++++-- tests/exports.v | 1 + 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/structures.v b/structures.v index 616cc505..be29618b 100644 --- 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 index b92d7de1..687e7028 100644 --- 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 *)