STRUCT: more

aya-prover · Sep 16, 2021 · 4f57875 · 4f57875
1 parent 17dc04d
commit 4f57875
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/base/src/main/java/org/aya/distill/CoreDistiller.java b/base/src/main/java/org/aya/distill/CoreDistiller.java
@@ -145,7 +145,7 @@ public record CoreDistiller(@NotNull DistillerOptions options) implements
 
   @Override
   public Doc visitFieldRef(@NotNull RefTerm.Field term, Boolean aBoolean) {
-    return varDoc(term.ref());
+    return linkRef(term.ref(), FIELD_CALL);
   }
 
   @Override public Doc visitError(@NotNull ErrorTerm term, Boolean aBoolean) {

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -64,7 +64,6 @@ public final class ExprTycker {
   public final @NotNull EqnSet termEqns = new EqnSet();
   public final @NotNull Sort.LvlVar universe = new Sort.LvlVar("u", null);
   public final @NotNull MutableMap<LevelGenVar, Sort.LvlVar> levelMapping = MutableMap.create();
-  private Term struct;
 
   private void tracing(@NotNull Consumer<Trace.@NotNull Builder> consumer) {
     if (traceBuilder != null) consumer.accept(traceBuilder);