Ignore:
Timestamp:
Apr 4, 2011, 5:13:09 PM (9 years ago)
Author:
campbell
Message:

Use more abstract identifiers in Clight / RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r729 r737  
    214214    | RTLabs.St_cost (lbl, _) ->
    215215        i+1,
    216         Printf.sprintf "%sdefinition C%s := ident_of_nat %d.\n%s"
     216        Printf.sprintf "%sdefinition C%s := costlabel_of_nat %d.\n%s"
    217217          (n_spaces n)
    218218          lbl
     
    314314
    315315let print_program p =
    316   Printf.sprintf "include \"RTLabs/import.ma\".\n\n(*program:*)\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n"
     316  Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n(*program:*)\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n"
    317317    (print_fun_decls 2 p.RTLabs.functs)
    318318    (print_fun 2 p.RTLabs.functs)
Note: See TracChangeset for help on using the changeset viewer.