aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorHugo Herbelin2014-10-21 11:07:48 +0200
committerHugo Herbelin2014-10-21 12:15:45 +0200
commitbe0121602ff9fb3200cafead25e325617164038a (patch)
tree34f5363c83df0ff7c852e4e619038187a3408948 /dev/include
parentda462f8a2b59a3d5ddd9f09add8a75f8e2624c9a (diff)
Continuing experimental printing of the signature of open evars in
Check (see cfff8f8a327) [printing only visible evars, not the ones corresponding to unrelated open goals + fixing bug on wrong sigma and on evar_info normalization].
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions