From 78102fedf6b1dca94cf2695bb1ba2000d4f76db9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jun 2016 15:08:16 +0200
Subject: Fixing bug in printing CannotSolveConstraint (collision of context
 names).

---
 toplevel/himsg.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3ff2d3fb18..fa47cc4311 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -67,10 +67,10 @@ let rec contract3' env a b c = function
   | NotSameArgSize | NotSameHead | NoCanonicalStructure
   | MetaOccurInBody _ | InstanceNotSameType _
   | UnifUnivInconsistency _ as x -> contract3 env a b c, x
-  | CannotSolveConstraint ((pb,env,t,u),x) ->
-      let env,t,u = contract2 env t u in
+  | CannotSolveConstraint ((pb,env',t,u),x) ->
+      let env',t,u = contract2 env' t u in
       let y,x = contract3' env a b c x in
-      y,CannotSolveConstraint ((pb,env,t,u),x)
+      y,CannotSolveConstraint ((pb,env',t,u),x)
 
 (** Printers *)
 
-- 
cgit v1.2.3