diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /ide/interface.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'ide/interface.mli')
-rw-r--r-- | ide/interface.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/ide/interface.mli b/ide/interface.mli index 6f7f1bcd..2a9b8b24 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -12,14 +12,15 @@ type raw = bool type verbose = bool +type richpp = Richpp.richpp (** The type of coqtop goals *) type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : string list; + goal_hyp : richpp list; (** List of hypotheses *) - goal_ccl : string; + goal_ccl : richpp; (** Goal conclusion *) } @@ -118,7 +119,7 @@ type edit_id = Feedback.edit_id should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * string) + | Fail of (state_id * location * richpp) type ('a, 'b) union = ('a, 'b) Util.union @@ -202,7 +203,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * string +type handle_exn_rty = state_id * location * richpp (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string |