diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:48 +0000 |
| commit | c46a640aaf9ec4fec52c5b76d32fce68414f6e7d (patch) | |
| tree | 697390d219b64dcc7ff979a7b8dad161da690359 /interp/modintern.ml | |
| parent | e8b2255678a7fa1c140c4a50dca26cc94ac1a6e0 (diff) | |
SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax
To retrieve the old behavior of spec_sub0 and spec_sub with
precondition on order, just chain spec_sub with Zmax_r or Zmax_l.
Idem with spec_pred0 and spec_pred.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12490 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/modintern.ml')
0 files changed, 0 insertions, 0 deletions