- Timestamp:
- Apr 19, 2011, 5:48:45 PM (10 years ago)
- Location:
- src/RTLabs
- Files:
-
- 1 edited
- 2 moved
-
import.ma (modified) (1 diff)
-
semantics.ma (moved) (moved from src/RTLabs/RTLabs-sem.ma) (1 diff)
-
syntax.ma (moved) (moved from src/RTLabs/RTLabs-syntax.ma)
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/import.ma
r750 r762 1 1 2 include "RTLabs/ RTLabs-sem.ma".2 include "RTLabs/semantics.ma". 3 3 4 4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝ -
src/RTLabs/semantics.ma
r761 r762 8 8 include "common/SmallstepExec.ma". 9 9 10 include "RTLabs/ RTLabs-syntax.ma".10 include "RTLabs/syntax.ma". 11 11 12 12 definition genv ≝ (genv_t Genv) (fundef internal_function).
Note: See TracChangeset
for help on using the changeset viewer.
