Changeset 1352 for src/RTLabs

Timestamp:

Oct 11, 2011, 12:45:16 PM (8 years ago)

Author:

sacerdot

Message:

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (1 diff)

src/RTLabs/RTLabsToRTL.ma

@@ -5 +5 @@
 include "common/Graphs.ma".
 include "joint/TranslateUtils.ma".
+include alias "ASM/BitVector.ma".
+include alias "arithmetics/nat.ma".
 
 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝