summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/coq/Semantics.v16
-rw-r--r--src/coq/Syntax.v2
2 files changed, 17 insertions, 1 deletions
diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v
index 2022ec94..19c67a05 100644
--- a/src/coq/Semantics.v
+++ b/src/coq/Semantics.v
@@ -209,5 +209,21 @@ Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
| right _ => fun x => x
end ((eDen e1) n)
+ | Concat c1 c2 e1 e2 => fun n =>
+ match (cDen c1) n as D return match D with
+ | None => unit
+ | Some T => T
+ end
+ -> match (match D with
+ | None => (cDen c2) n
+ | v => v
+ end) with
+ | None => unit
+ | Some T => T
+ end with
+ | None => fun _ => (eDen e2) n
+ | _ => fun x => x
+ end ((eDen e1) n)
+
| _ => cheat _
end.
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.