diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-05-31 09:28:17 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:35 -0400 |
| commit | 6ea16dcd9d9635283d0b2146edb6a29bd3ee0933 (patch) | |
| tree | 73d4906d9f6cdeb13cd462bf19101aa91558f59c /src/Assembly/Pseudo.v | |
| parent | 63744c51fb183c7701edd6e2eece594946170786 (diff) | |
Generalized and cleaned up state model
Pseudo conversions
Diffstat (limited to 'src/Assembly/Pseudo.v')
| -rw-r--r-- | src/Assembly/Pseudo.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index a0ebf7255..21cc11c4e 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -29,7 +29,7 @@ Module Pseudo (M: PseudoMachine) <: Language. | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m | PComb: forall n a b, Pseudo n a -> Pseudo n b -> Pseudo n (a + b) - | PCall: forall n m, Pseudo n m -> Pseudo n m. + | PCall: forall n m, Label -> Pseudo n m -> Pseudo n m. Hint Constructors Pseudo. @@ -101,7 +101,7 @@ Module Pseudo (M: PseudoMachine) <: Language. funexpseudo e'' st'') end) e st - | PCall n m p => pseudoEval p st + | PCall n m _ p => pseudoEval p st end. Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st'). |