Changeset 474


Ignore:
Timestamp:
Jan 21, 2011, 2:31:00 PM (6 years ago)
Author:
campbell
Message:

Reduce "include"s to reduce compilation time.
(Will be undone when moving to the new-new system.)

Location:
Deliverables/D3.1/C-semantics
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r457 r474  
    1616(* * Dynamic semantics for the Clight language *)
    1717
    18 include "Coqlib.ma".
    19 include "Errors.ma".
    20 include "Integers.ma".
    21 include "Floats.ma".
    22 include "Values.ma".
    23 include "AST.ma".
    24 include "Mem.ma".
     18(*include "Coqlib.ma".*)
     19(*include "Errors.ma".*)
     20(*include "Integers.ma".*)
     21(*include "Floats.ma".*)
     22(*include "Values.ma".*)
     23(*include "AST.ma".*)
     24(*include "Mem.ma".*)
    2525include "Globalenvs.ma".
    2626include "Csyntax.ma".
    2727include "Maps.ma".
    28 include "Events.ma".
     28(*include "Events.ma".*)
    2929include "Smallstep.ma".
    3030
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r255 r474  
    1616(* * Abstract syntax for the Clight language *)
    1717
    18 include "Integers.ma".
     18(*include "Integers.ma".*)
    1919include "AST.ma".
    2020include "Coqlib.ma".
  • Deliverables/D3.1/C-semantics/Events.ma

    r379 r474  
    1818Require Import Coqlib.
    1919*)
    20 include "AST.ma".
    21 include "Integers.ma".
    22 include "Floats.ma".
     20(*include "AST.ma".*)
     21(*include "Integers.ma".*)
     22(*include "Floats.ma".*)
    2323include "Values.ma".
    2424include "datatypes/list.ma".
  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r467 r474  
    3636include "Errors.ma".
    3737include "AST.ma".
    38 include "Values.ma".
     38(*include "Values.ma".*)
    3939include "Mem.ma".
    4040
  • Deliverables/D3.1/C-semantics/Mem.ma

    r456 r474  
    2626
    2727include "arithmetics/nat.ma".
    28 include "binary/Z.ma".
    29 include "datatypes/sums.ma".
    30 include "datatypes/list.ma".
    31 include "Plogic/equality.ma".
    32 
    33 include "Coqlib.ma".
     28(*include "binary/Z.ma".*)
     29(*include "datatypes/sums.ma".*)
     30(*include "datatypes/list.ma".*)
     31(*include "Plogic/equality.ma".*)
     32
     33(*include "Coqlib.ma".*)
    3434include "Values.ma".
    35 include "AST.ma".
     35(*include "AST.ma".*)
    3636include "extralib.ma".
    3737
  • Deliverables/D3.1/C-semantics/depends

    r473 r474  
    11SmallstepExec.ma Events.ma IOMonad.ma Integers.ma extralib.ma
    2 Mem.ma AST.ma Coqlib.ma Plogic/equality.ma Values.ma arithmetics/nat.ma binary/Z.ma datatypes/list.ma datatypes/sums.ma extralib.ma
     2Mem.ma Values.ma arithmetics/nat.ma extralib.ma
    33IOMonad.ma Errors.ma Plogic/russell_support.ma extralib.ma
    44Integers.ma arithmetics/nat.ma binary/Z.ma extralib.ma
     
    1616Animation.ma Cexec.ma
    1717CexecComplete.ma Cexec.ma Plogic/connectives.ma
    18 Globalenvs.ma AST.ma Errors.ma Mem.ma Values.ma
     18Globalenvs.ma AST.ma Errors.ma Mem.ma
    1919Maps.ma AST.ma Coqlib.ma
    20 Events.ma AST.ma CostLabel.ma Floats.ma Integers.ma Values.ma datatypes/list.ma extralib.ma
     20Events.ma CostLabel.ma Values.ma datatypes/list.ma extralib.ma
    2121Values.ma AST.ma Coqlib.ma Floats.ma Integers.ma Plogic/connectives.ma
    2222extralib.ma Plogic/equality.ma binary/Z.ma binary/positive.ma datatypes/list.ma datatypes/sums.ma
    23 Csyntax.ma AST.ma Coqlib.ma CostLabel.ma Errors.ma Integers.ma
    24 Csem.ma AST.ma Coqlib.ma Csyntax.ma Errors.ma Events.ma Floats.ma Globalenvs.ma Integers.ma Maps.ma Mem.ma Smallstep.ma Values.ma
     23Csyntax.ma AST.ma Coqlib.ma CostLabel.ma Errors.ma
     24Csem.ma Csyntax.ma Globalenvs.ma Maps.ma Smallstep.ma
    2525Plogic/connectives.ma
    2626Plogic/equality.ma
Note: See TracChangeset for help on using the changeset viewer.