theories/base_logic/fixpoint.v · 7a58ae18892816cf494aa834e706a6b10200b1c0 · Simcha van Collem / Iris

Forked from Iris / Iris

Source project has a limited visibility.

7 years ago

Rename fix.v → fixpoint.v because fix is a reserved keyword. · 7a58ae18

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]).

7a58ae18

History

Rename fix.v → fixpoint.v because fix is a reserved keyword.

Robbert Krebbers authored 7 years ago

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]).