Continuing experimentation on what part of the instance of an evar

to display by default (see bc8a5357889 - 17 Oct 2014):
- not printing instances for let-in anymore even when expanded (since
  they are canonical up to conversion)
- still printing x:=x in [x:=x;x':=x] when x is directly an instance
  of another var, but not in [x:=x;x':=S x]
  This can be discussed, but if ever this is to be changed, it should
  not be printed in [x:=x;x:=?n] with ?n implicitly depending on x
  (otherwise said, variables which are not displayed in instances of
  internal evars should not contribute to the decision of writing
  x:=x in the instance).

1 files changed, 1 insertions, 1 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 58e1eb1d17..f57772ecb0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -977,7 +977,7 @@ let rec glob_of_pat env sigma = function
   | PRef ref -> GRef (loc,ref,None)
   | PVar id -> GVar (loc,id)
   | PEvar (evk,l) ->
-      let test id = function PVar id' -> Id.equal id id' | _ -> false in
+      let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
       let id = Evd.evar_ident evk sigma in
       GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)