diff options
author | 2014-10-17 15:12:02 +0200 | |
---|---|---|
committer | 2014-10-17 15:12:05 +0200 | |
commit | bc8a5357889396f07d005a84bd3c50e9a25c1ddb (patch) | |
tree | 63bd14d10d345d9a1548626301632d8deb833835 | |
parent | 239cf334fcc844f06a9e6ea2e6745d2fa8915325 (diff) |
New experimental heuristic printing strategy for evar instances: We
don't print bindings of the form "x:=x" unless there is also a binding
"x':=x". Otherwise said, if a variable occurs several time, the
binding where it occurs under the form "x:=x" is printed anyway. This
should help to understand where the instance is non trivial while
still not obfuscating display in goals with very long list of
uninteresting trivial instances.
-rw-r--r-- | pretyping/detyping.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 605d59135..e9a1174b4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -491,18 +491,20 @@ let rec detype flags avoid env sigma t = else noparams () | Evar (evk,cl) -> + let bound_to_itself id c = + try let n = List.index Name.equal (Name id) (fst env) in + isRelN n c + with Not_found -> isVarId id c in let id,l = - try Evd.evar_ident evk sigma, - Evd.evar_instance_array - (fun id c -> - try let n = List.index Name.equal (Name id) (fst env) in - isRelN n c - with Not_found -> isVarId id c) - (Evd.find sigma evk) cl + 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 -> 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 + id,l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), - (List.map_i (fun i c -> (Id.of_string ("A" ^ string_of_int i),c)) - 1 (Array.to_list cl)) + (Array.map_to_list (fun c -> (Id.of_string "A",c)) cl) in GEvar (dl,id, List.map (on_snd (detype flags avoid env sigma)) l) |