diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-02-21 13:22:30 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-02-21 13:22:30 -0500 |
| commit | fe5ac0fba7f973b2557c7ae7a6bb9248024ffacd (patch) | |
| tree | 1ffa812bdb1fcfc087d3c83b948c32f66023ebc8 /src/coq/Syntax.v | |
| parent | 8794ce0f4d86c23e15314141e3638d99277e2ad0 (diff) | |
Time to start thinking about guards
Diffstat (limited to 'src/coq/Syntax.v')
| -rw-r--r-- | src/coq/Syntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v index 13b7e9de..b19a790e 100644 --- a/src/coq/Syntax.v +++ b/src/coq/Syntax.v @@ -187,6 +187,6 @@ Section vars. | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _))) | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c') - | Concat : forall c1 c2, disj c1 c2 -> exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) + | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c). End vars. |