Mercurial > urweb
diff src/coq/Syntax.v @ 619:f38e009009bb
Time to start thinking about guards
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 21 Feb 2009 13:22:30 -0500 |
| parents | be88d2d169f6 |
| children | d828b143e147 |
line wrap: on
line diff
--- a/src/coq/Syntax.v Sat Feb 21 13:17:06 2009 -0500 +++ b/src/coq/Syntax.v Sat Feb 21 13:22:30 2009 -0500 @@ -187,6 +187,6 @@ | 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.