diff options
author | 2015-02-21 17:05:53 +0100 | |
---|---|---|
committer | 2015-02-21 17:06:49 +0100 | |
commit | dd888dffd48fbf74a83b9f3c07bbdeb63dc020a2 (patch) | |
tree | 52448f53b692d3bbff4d87a09f15adac87211afe /pretyping/detyping.ml | |
parent | cf6a68b45b506be1dc2d37b0daefeaf18ff7c77a (diff) |
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).
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r-- | pretyping/detyping.ml | 11 |
1 files changed, 6 insertions, 5 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)), |