Merge branch 'master' into highprecision

nickbattle · Dec 1, 2023 · f1ac513 · f1ac513
2 parents 894d834 + c6e32b9
commit f1ac513
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java
@@ -51,6 +51,7 @@
 import com.fujitsu.vdmj.typechecker.Environment;
 import com.fujitsu.vdmj.typechecker.NameScope;
 import com.fujitsu.vdmj.typechecker.TypeChecker;
+import com.fujitsu.vdmj.typechecker.TypeComparator;
 
 @SuppressWarnings("serial")
 public class ProofObligationList extends Vector<ProofObligation>
@@ -183,7 +184,10 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env
 		// Some POs from VDM++ specs can include "new" etc, so parse as the given dialect
 		LexTokenReader ltr = new LexTokenReader(obligation.getValue(), Settings.dialect);
 		ExpressionReader reader = new ExpressionReader(ltr);
+
+		// Treat the PO as if it is an expression within the module that defines it.
 		reader.setCurrentModule(mname);
+		TypeComparator.setCurrentModule(mname);
 
 		boolean oldmax = Properties.parser_maximal_types;
 		Properties.parser_maximal_types = true;		// For parse of PO on inv_T(T!)