Fix bugs in module loading

JetBrains · Mar 19, 2024 · da10a8b · da10a8b
1 parent 7b81857
commit da10a8b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/base/src/main/java/org/arend/library/BaseLibrary.java b/base/src/main/java/org/arend/library/BaseLibrary.java
@@ -68,6 +68,9 @@ public void resetGroup(Group group) {
     for (Group subgroup : group.getDynamicSubgroups()) {
       resetGroup(subgroup);
     }
+    for (Group.InternalReferable referable : group.getInternalReferables()) {
+      resetDefinition(referable.getReferable());
+    }
   }
 
   public void resetDefinition(LocatedReferable referable) {

diff --git a/base/src/main/java/org/arend/naming/reference/MetaReferable.java b/base/src/main/java/org/arend/naming/reference/MetaReferable.java
@@ -141,6 +141,6 @@ public MetaTopDefinition getTypechecked() {
   @Override
   public boolean isTypechecked() {
     // If it's a definable meta, we always need to typecheck its dependencies
-    return myDefinition != null && (!(myDefinition instanceof DefinableMetaDefinition) || myTypechecked != null);
+    return myDefinition != null && (!(myDefinition instanceof DefinableMetaDefinition) || myTypechecked != null && !myTypechecked.status().needsTypeChecking());
   }
 }