aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evarutil.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-25 16:37:55 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-25 21:30:09 +0200
commit4f392bc8114309f388791c1ddc7cc95cc021aa5e (patch)
tree5d002b17dbecea4ccee77afeb26debc2458a9021 /engine/evarutil.mli
parent9e1372f77218ca6f0baf4ed7c590c91ad84b6313 (diff)
Reorganizing functions to find the relative position of an hypothesis.
Also fixing a bug of get_next_hyp_position when the hypothesis is the oldest of the context (see test in ltac.v).
Diffstat (limited to 'engine/evarutil.mli')
0 files changed, 0 insertions, 0 deletions