summaryrefslogtreecommitdiff
path: root/toplevel/himsg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r--toplevel/himsg.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a97bf9bb..a080442c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: himsg.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Pp
open Util
@@ -543,7 +543,7 @@ let explain_unsatisfiable_constraints env evd constr =
match constr with
| None ->
str"Unable to satisfy the following constraints:" ++ fnl() ++
- pr_constraints true env evm
+ pr_constraints true env undef
| Some (ev, k) ->
explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++
if List.length (Evd.to_list undef) > 1 then