diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /ide/coq.mli | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (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.mli | 8 |
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 |