Fixing #3634 (wrong env in "cannot instantiate because not in its

scope" error message).

4 files changed, 10 insertions, 9 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 94ec82029..621174aaa 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1532,7 +1532,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
       reconsider_conv_pbs conv_algo evd
   with
     | NotInvertibleUsingOurAlgorithm t ->
-        UnifFailure (evd,NotClean (ev1,t))
+        UnifFailure (evd,NotClean (ev1,env,t))
     | OccurCheckIn (evd,rhs) ->
         UnifFailure (evd,OccurCheck (evk1,rhs))
     | MetaOccurInBodyInternal ->
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cad0beabf..e16d1206a 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,7 +14,7 @@ open Type_errors
 
 type unification_error =
   | OccurCheck of existential_key * constr
-  | NotClean of existential * constr
+  | NotClean of existential * env * constr
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index cc1443162..b74ca1936 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -15,7 +15,7 @@ open Type_errors
 
 type unification_error =
   | OccurCheck of existential_key * constr
-  | NotClean of existential * constr
+  | NotClean of existential * env * constr
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 15d6e29eb..90df17427 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -51,15 +51,16 @@ let contract3 env a b c = match contract env [a;b;c] with
 let contract4 env a b c d = match contract env [a;b;c;d] with
   | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false
 
-let contract4_vect env a b c d v =
-  match contract env ([a;b;c;d] @ Array.to_list v) with
-  | env, a::b::c::d::l -> (env,a,b,c),d,Array.of_list l
+let contract1_vect env a v =
+  match contract env (a :: Array.to_list v) with
+  | env, a::l -> env,a,Array.of_list l
   | _ -> assert false
 
 let contract3' env a b c = function
   | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d)
-  | NotClean ((evk,args),d) ->
-      let x,d,args = contract4_vect env a b c d args in x,NotClean((evk,args),d)
+  | NotClean ((evk,args),env',d) ->
+      let env',d,args = contract1_vect env' d args in
+      contract3 env a b c,NotClean((evk,args),env',d)
   | ConversionFailed (env',t1,t2) ->
       let (env',t1,t2) = contract2 env' t1 t2 in
       contract3 env a b c, ConversionFailed (env',t1,t2)
@@ -264,7 +265,7 @@ let explain_unification_error env sigma p1 p2 = function
         spc () ++ str "(cannot define " ++ quote (pr_existential_key sigma evk) ++
 	strbrk " with term " ++ pr_lconstr_env env sigma rhs ++
         strbrk " that would depend on itself)"
-    | NotClean ((evk,args),c) ->
+    | NotClean ((evk,args),env,c) ->
         let c = Evarutil.nf_evar sigma c in
         let args = Array.map (Evarutil.nf_evar sigma) args in
         spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key sigma evk)