Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
That caused some problems, e.g.: From iris.base_logic Require Export fix. Gave: Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).
Robbert Krebbers authoredThat caused some problems, e.g.: From iris.base_logic Require Export fix. Gave: Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).