diff options
Diffstat (limited to 'lib/interface.mli')
| -rw-r--r-- | lib/interface.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index a01ec20aed..8d250f8507 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -127,6 +127,8 @@ type edit_or_state_id = Edit of edit_id | State of state_id type feedback_content = | AddedAxiom | Processed + | Incomplete + | Complete | GlobRef of Loc.t * string * string * string * string | ErrorMsg of Loc.t * string | InProgress of int |