aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--frontend/syntax.dcl1
-rw-r--r--frontend/syntax.icl1
2 files changed, 2 insertions, 0 deletions
diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl
index d63f836..4579a4b 100644
--- a/frontend/syntax.dcl
+++ b/frontend/syntax.dcl
@@ -865,6 +865,7 @@ cNonRecursiveAppl :== False
| TVI_Used /* to administer that this variable is encountered (in checkOpenTypes) */
| TVI_TypeCode !TypeCodeExpression
| TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */
+ | TVI_Normalized !Int /* MV - position of type variable in its definition */
:: TypeVarInfoPtr :== Ptr TypeVarInfo
:: TypeVarHeap :== Heap TypeVarInfo
diff --git a/frontend/syntax.icl b/frontend/syntax.icl
index 7859e21..2964ebd 100644
--- a/frontend/syntax.icl
+++ b/frontend/syntax.icl
@@ -835,6 +835,7 @@ cNotVarNumber :== -1
| TVI_Used /* to adminster that this variable is encountered (in checkOpenTypes) */
| TVI_TypeCode !TypeCodeExpression
| TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */
+ | TVI_Normalized !Int /* MV - position of type variable in its definition */
:: TypeVarInfoPtr :== Ptr TypeVarInfo
:: TypeVarHeap :== Heap TypeVarInfo