From dd888dffd48fbf74a83b9f3c07bbdeb63dc020a2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Feb 2015 17:05:53 +0100
Subject: 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).

---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

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)
-- 
cgit v1.2.3