diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli index 879323a37d..e518cf583f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3714,6 +3714,7 @@ sig | 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 = | VtKeep |