Changeset 173


Ignore:
Timestamp:
Oct 13, 2010, 12:12:53 PM (9 years ago)
Author:
campbell
Message:

Minor changes for newer versions of matita.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Coqlib.ma

    r24 r173  
    2121include "datatypes/sums.ma".
    2222include "datatypes/list.ma".
     23include "datatypes/list-theory.ma".
    2324
    2425include "extralib.ma".
  • C-semantics/extralib.ma

    r16 r173  
    518518##| #n'; nelim m;
    519519  ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
    520   ##| #m' IH dv md; nnormalize;
     520  ##| #m' IH dv md; nwhd in ⊢ (??%? → ?(???%)?);
    521521      nlapply (refl ? (divide m' (succ n')));
    522522      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
    523523      #dv' md' DIVr; nelim (IH … DIVr);
    524       nnormalize; ncases md';
     524      nwhd in ⊢ (? → ? → ??%? → ?);
     525      ncases md';
    525526      ##[ ncases dv'; nnormalize;
    526527        ##[ #H; ndestruct;
     
    532533          nlapply (partial_minus_to_Prop md'' n);
    533534          ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
    534           #lt; #e; ndestruct; @; /2/; napply plt_pos;
     535          #lt; #e; ndestruct; @; ##[ /3/; ##| ##*: /2/; ##] napply plt_pos;
    535536          ##[ ##1,3,5,7: napply double_lt1; /2/;
    536537          ##| ##2,4: napply double_lt3; /2/;
Note: See TracChangeset for help on using the changeset viewer.