aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.mli
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /ide/coq.mli
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index df369cc18..c2f96a1fe 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -42,15 +42,15 @@ val reset_initial : unit -> unit
val reset_to : reset_mark -> unit
val reset_to_mod : identifier -> unit
-val init : unit -> string list
+val init : unit -> string list
val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr)
val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
-val interp_and_replace : string ->
+val interp_and_replace : string ->
(reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string
(* type hyp = (identifier * constr option * constr) * string *)
-type hyp = env * evar_map *
+type hyp = env * evar_map *
((identifier*string) * constr option * constr) * (string * string)
type meta = env * evar_map * string
type concl = env * evar_map * constr * string
@@ -74,7 +74,7 @@ val is_in_loadpath : string -> bool
val make_cases : string -> string list list
-type tried_tactic =
+type tried_tactic =
| Interrupted
| Success of int (* nb of goals after *)
| Failed