Changeset 1612


Ignore:
Timestamp:
Dec 14, 2011, 3:58:39 PM (8 years ago)
Author:
sacerdot
Message:

All library ported to new Matita lib (finally).

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1608 r1612  
    874874    | Some e1 ⇒
    875875        do e1' ← translate_expr vars e1;
    876         OK ? «〈St_return (Some ? (mk_Sig … e1')), u〉, ?»
     876        OK ? «〈St_return (Some ? (mk_DPair … e1')), u〉, ?»
    877877    ]
    878878| Sswitch e1 ls ⇒ Error ? (msg FIXME)
     
    928928| #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
    929929(* Slabel *)
    930 |31: %{l} @E
    931 |32: @(π1 (π1 H1))
    932 |33: #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
    933 |34: @(π2 H1)
     930| %{l} @E
     931| @(π1 (π1 H1))
     932| #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
     933| @(π2 H1)
    934934(* Sgoto *)
    935 |35: %{l} @E
    936 |36: @(π1 (π1 H1))
     935| %{l} @E
     936| @(π1 (π1 H1))
    937937(* Scost *)
    938 |37: @(π2 (π1 H1))
    939 |38: @(π2 H1)
    940 |*: cases daemon (*XXXXX*)
     938| @(π2 (π1 H1))
     939| @(π2 H1)
    941940] qed.
    942941
  • src/RTLabs/import.ma

    r1072 r1612  
    8888         (pf_stacksize pre_f)
    8989         graph
    90          (dp ?? entry p)
    91          (dp ?? exit q)
     90         (mk_Sig ?? entry p)
     91         (mk_Sig ?? exit q)
    9292         )))
    9393   .
Note: See TracChangeset for help on using the changeset viewer.