diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-11 15:08:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-12 12:48:26 +0200 |
| commit | 78102fedf6b1dca94cf2695bb1ba2000d4f76db9 (patch) | |
| tree | e9c459f3e9ca5aa2e50a9b8f57c5d25c72a8f5dc | |
| parent | f9695eb4bc5b377a02f49ee485d7fe9be122c183 (diff) | |
Fixing bug in printing CannotSolveConstraint (collision of context names).
| -rw-r--r-- | toplevel/himsg.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3ff2d3fb1..fa47cc431 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 *) |