diff options
Diffstat (limited to 'ide/interface.mli')
| -rw-r--r-- | ide/interface.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ide/interface.mli b/ide/interface.mli index 1a4d6c0ecb..1939a8427c 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,9 +17,9 @@ type verbose = bool type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : Pp.std_ppcmds list; + goal_hyp : Pp.t list; (** List of hypotheses *) - goal_ccl : Pp.std_ppcmds; + goal_ccl : Pp.t; (** Goal conclusion *) } @@ -121,7 +121,7 @@ type edit_id = int should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * Pp.std_ppcmds) + | Fail of (state_id * location * Pp.t) type ('a, 'b) union = ('a, 'b) Util.union @@ -213,7 +213,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * Pp.std_ppcmds +type handle_exn_rty = state_id * location * Pp.t (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string |