Command: Init - siegebell/vscoq GitHub Wiki

Init()

No options.

<call val="Init"><option val="none"/></call>

With options. Looking at ide_slave.ml, it seems that options is just the name of a *.v file, whose path is added via Add LoadPath to the initial state.

<call val="Init">
  <option val="some">
    <string>${options}</string>
  </option>
</call>

Returns

The initial stateId (not associated with a sentence)

<value val="good">
  <state_id val="${initialStateId}"/>
</value>

⚠️ GitHub.com Fallback ⚠️