summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/monoize.sml2
-rw-r--r--src/unnest.sml13
2 files changed, 10 insertions, 5 deletions
diff --git a/src/monoize.sml b/src/monoize.sml
index ee509f52..a4f38dc6 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -406,7 +406,7 @@ fun fooifyExp fk env =
fm)
end
- | _ => (E.errorAt loc "Don't know how to encode attribute type";
+ | _ => (E.errorAt loc "Don't know how to encode attribute/URL type";
Print.eprefaces' [("Type", MonoPrint.p_typ MonoEnv.empty tAll)];
(dummyExp, fm))
in
diff --git a/src/unnest.sml b/src/unnest.sml
index fe63f9fe..8e363301 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -206,6 +206,14 @@ fun exp ((ks, ts), e as old, st : state) =
val loc = #2 ed
val nr = length vis
+ val subsLocal = List.filter (fn (_, (ERel _, _)) => false
+ | _ => true) subs
+ val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e))
+ subsLocal
+
+ val vis = map (fn (x, t, e) =>
+ (x, t, doSubst' (e, subsLocal))) vis
+
val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
let
val (cfv', efv') = fvsExp nr e
@@ -243,15 +251,12 @@ fun exp ((ks, ts), e as old, st : state) =
maxName + 1))
maxName vis
-
-
val subs = map (fn (n, e) => (n + nr,
case e of
(ERel _, _) => e
| _ => liftExpInExp nr 0 e))
subs
-
val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
let
val e = (ENamed n, loc)
@@ -278,7 +283,7 @@ fun exp ((ks, ts), e as old, st : state) =
let
(*val () = Print.prefaces "preSubst"
[("e", ElabPrint.p_exp E.empty e)]*)
- val e = doSubst' (e, subs)
+ val e = doSubst' (e, subs')
(*val () = Print.prefaces "squishCon"
[("t", ElabPrint.p_con E.empty t)]*)