diff options
| author | Talia Ringer | 2019-05-22 16:09:51 -0400 |
|---|---|---|
| committer | Talia Ringer | 2019-05-22 16:09:51 -0400 |
| commit | 577db38704896c75d1db149f6b71052ef47202be (patch) | |
| tree | 946afdb361fc9baaa696df7891d0ddc03a4a8594 /stm/stm.mli | |
| parent | 7eefc0b1db614158ed1b322f8c6e5601e3995113 (diff) | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Merge remote-tracking branch 'origin/master' into stm+doc_hook
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 01bedb4fd8..06d3d28057 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -111,7 +111,7 @@ val parse_sentence : If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_control CAst.t -> + bool -> Vernacexpr.vernac_control -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* Returns the proof state before the last tactic that was applied at or before @@ -175,7 +175,7 @@ val get_current_state : doc:doc -> Stateid.t val get_ldir : doc:doc -> Names.DirPath.t (* This returns the node at that position *) -val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option +val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option (* Filename *) val set_compilation_hints : string -> unit @@ -301,7 +301,7 @@ val restore : document -> unit (** Experimental Hooks for UI experiment plugins, not for general use! *) type document_edit_notifiers = - { add_hook : Vernacexpr.vernac_control CAst.t -> Stateid.t -> unit + { add_hook : Vernacexpr.vernac_control -> Stateid.t -> unit (** User adds a sentence to the document (after parsing) *) ; edit_hook : Stateid.t -> unit (** User edits a sentence in the document *) |