wip

math-comp · Dec 4, 2023 · a97ee8d · a97ee8d
1 parent cb89401
commit a97ee8d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/structures.v b/structures.v
@@ -665,7 +665,7 @@ actions N :-
   coq.env.current-library File,
   coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)),
   coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File O)),
-  if (get-option "mathcomp" tt) (actions-compat N) true.
+  if (get-option "mathcomp" tt ; get-option "mathcomp.axiom" _) (actions-compat N) true.
 
 pred actions-compat i:id.
 actions-compat ModuleName :-