summaryrefslogtreecommitdiff
path: root/toplevel/himsg.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
commite4282ea99c664d8d58067bee199cbbcf881b60d5 (patch)
treed4c4a873eb055c728666f367469fa26c3417793a /toplevel/himsg.ml
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r--toplevel/himsg.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f733a3d5..0cda7c71 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: himsg.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: himsg.ml 11986 2009-03-17 11:44:20Z herbelin $ *)
open Pp
open Util
@@ -814,8 +814,8 @@ let explain_ltac_call_trace (last,trace,loc) =
(if unboundvars <> [] or vars <> [] then
strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) ->
pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
- (List.rev vars @ unboundvars)
- else mt()) ++ str ")" in
+ (List.rev vars @ unboundvars) ++ str ")"
+ else mt()) in
if calls <> [] then
let kind_of_last_call = match list_last calls with
| Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."