Changeset 1348 for src/RTL

Timestamp:

Oct 10, 2011, 10:40:08 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• src/RTL/RTL.ma (modified) (1 diff)

src/RTL/RTL.ma

@@ -31 +31 @@
   To be fixed once we understand exactly what to do with tail calls. *)
 inductive rtlntc_statement_extension: Type[0] ≝
-  | rtlntc_st_ext_address: register → register → rtlntc_statement_extension
+  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.