diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-01 10:52:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-01 10:54:53 +0100 |
| commit | c17c3faee20251cd5c7168246e9ffcd12d557f85 (patch) | |
| tree | 02635866b73d7595fad009cc17535a6bbf06c2fc /ide | |
| parent | f86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff) | |
| parent | 568b38e1d599f8bac5adf140f5a114f2871bc436 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/interface.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/interface.mli b/ide/interface.mli index 2a9b8b241..123cac6c2 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -139,7 +139,7 @@ type add_rty = state_id * ((unit, state_id) union * string) [Inr (start,(stop,tip))] if [id] is in a zone that can be focused. In that case the zone is delimited by [start] and [stop] while [tip] is the new document [tip]. Edits made by subsequent [add] are always - performend on top of [id]. *) + performed on top of [id]. *) type edit_at_sty = state_id type edit_at_rty = (unit, state_id * (state_id * state_id)) union @@ -153,7 +153,7 @@ type query_rty = string type goals_sty = unit type goals_rty = goals option -(** Retrieve the list of unintantiated evars in the current proof. [None] if no +(** Retrieve the list of uninstantiated evars in the current proof. [None] if no proof is in progress. *) type evars_sty = unit type evars_rty = evar list option |