aboutsummaryrefslogtreecommitdiff
path: root/lib/cArray.ml
diff options
context:
space:
mode:
authorHugo Herbelin2014-10-02 11:32:56 +0200
committerHugo Herbelin2014-10-02 16:17:29 +0200
commitf65318d2036ebe26d1c537f2fd04410b32d4ff86 (patch)
treefe0a63e729887bfacf3c1f55c8c5bb3763b72251 /lib/cArray.ml
parent8a382c1906728f89b13d20f541137a670d2c3c75 (diff)
Revert "test-suite: New names for vars but the expected invariant is preserved"
This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf. Going back to the convention of naming bound variables in hypotheses of the goal as in 8.4. My arguments for the revert are: - apply ... with (id:=...) would have to be changed too, then possibly breaking the compatibility - the naming became dependent of the order of variables as in x:nat H:forall x0, x0=0 ===== goal but H:forall x, x=0 x:nat ===== goal Accordingly, this is all a matter of convention, since the meaning of bindings is anyway the same in both cases.
Diffstat (limited to 'lib/cArray.ml')
0 files changed, 0 insertions, 0 deletions