diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index e518cf583f..535f6a29bb 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3713,7 +3713,6 @@ sig | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtBack of vernac_part_of_script * Stateid.t | VtMeta | VtUnknown and vernac_qed_type = |
