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).

3 files changed, 12 insertions, 11 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 046ee0dad..28fb8cbe3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -498,16 +498,17 @@ let rec detype flags avoid env sigma t =
 	  else noparams ()
 
     | Evar (evk,cl) ->
-        let bound_to_itself id c =
+        let bound_to_itself_or_letin (id,b,_) c =
+          b != None ||
 	  try let n = List.index Name.equal (Name id) (fst env) in 
-	      isRelN n c 
+	      isRelN n c
 	  with Not_found -> isVarId id c in
       let id,l =
         try
           let id = Evd.evar_ident evk sigma in
-          let l = Evd.evar_instance_array bound_to_itself (Evd.find sigma evk) cl in
-          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> (Id.Set.union fvs (collect_vars c), Int.Set.union rels (free_rels c))) (Id.Set.empty,Int.Set.empty) l in
-          let l = Evd.evar_instance_array (fun id c -> not !print_evar_arguments && (bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
+          let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
+          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
+          let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ee72d3147..9313e2232 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -230,20 +230,20 @@ let evar_instance_array test_id info args =
     else instance_mismatch ()
   | false :: filter, _ :: ctxt ->
     instrec filter ctxt i
-  | true :: filter, (id, _, _) :: ctxt ->
+  | true :: filter, (id,_,_ as d) :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
-      if test_id id c then instrec filter ctxt (succ i)
+      if test_id d c then instrec filter ctxt (succ i)
       else (id, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-    let map i (id, _, _) =
+    let map i (id,_,_ as d) =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id id c then None else Some (id,c)
+        if test_id d c then None else Some (id,c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -251,7 +251,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array isVarId info args
+  evar_instance_array (fun (id,_,_) -> isVarId id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index b6c5d426f..cf6ba07c6 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -223,7 +223,7 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr