coq export: use Require Import instead of Require Export#1158

Merged

fblanqui merged 1 commit intoDeducteam:masterfrom fblanqui:coq

Nov 28, 2024

+1-1

Commits on Nov 28, 2024

partially revert previous commit: use Require Import instead of Require Export for efficiency reason
fblanqui
committed