aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-21 17:05:53 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-21 17:06:49 +0100
commitdd888dffd48fbf74a83b9f3c07bbdeb63dc020a2 (patch)
tree52448f53b692d3bbff4d87a09f15adac87211afe /pretyping/coercion.ml
parentcf6a68b45b506be1dc2d37b0daefeaf18ff7c77a (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/coercion.ml')
0 files changed, 0 insertions, 0 deletions